Commit 2023-08-07 08:44 5759caed
View on Github →feat: two easy lemmas about List.Lex (#6395)
Proves that []
is the "bottom element" for List.Lex r
for any relation r
and that List.Lex r [a] [b]
iff r a b
feat: two easy lemmas about List.Lex (#6395)
Proves that []
is the "bottom element" for List.Lex r
for any relation r
and that List.Lex r [a] [b]
iff r a b