Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-11-05 07:05:32 +03:00
Code Issues Projects Releases Wiki Activity

readd missing proof

Browse Source
This commit is contained in:
Rígille S. B. Menezes 2021-11-25 15:00:02 -03:00
parent d4ea067d3d
commit 6728e3b020
1 changed files with 10 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
base/List/concat/nil_right.kind Normal file
View File

@ -0,0 +1,10 @@
List.concat.nil_right<A: Type>(l: List<A>): l == l ++ []
case l {
nil:
refl
cons:
case List.concat.nil_right<A>(l.tail) {
refl:
refl
}: Equal(List<A>, List.cons(A, l.head, l.tail), List.cons(A, l.head, self.b))
}!