\ / GNU General Public License Version 2
V_______________________________________________________________ *)
-include "arithmetics/nat.ma".\ 5span class="error" title="disambiguation error"\ 6\ 5/span\ 6
+include "arithmetics/nat.ma".
inductive list (A:Type[0]) : Type[0] :=
| nil: list A
\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i∈(I\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6J)} (f i).
#A #B #I #J #nil #op #f (elim I) normalize
[>\ 5a href="cic:/matita/basics/list/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6 //|#a #tl #Hind <\ 5a href="cic:/matita/basics/list/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
-qed.
\ No newline at end of file
+qed.