+record Aop (A:Type[0]) (nil:A) : Type[0] ≝
+{op :2> A → A → A;
+ nill:∀a. op nil a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+ nilr:∀a. op a nil \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 a;
+ assoc: ∀a,b,c.op a (op b c) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 op (op a b) c
+}.
+
+theorem fold_sum: ∀A,B. ∀I,J:\ 5a href="cic:/matita/tutorial/chapter3/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀nil.∀op:\ 5a href="cic:/matita/tutorial/chapter3/Aop.ind(1,0,2)"\ 6Aop\ 5/a\ 6 B nil.∀f:A → B.
+ op (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ I} (f i)) (\ 5a title="\fold" href="cic:/fakeuri.def(1)"\ 6\fold\ 5/a\ 6[op,nil]_{i ∈ J} (f i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6
+ \ 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/tutorial/chapter3/nill.fix(0,2,2)"\ 6nill\ 5/a\ 6//|#a #tl #Hind <\ 5a href="cic:/matita/tutorial/chapter3/assoc.fix(0,2,2)"\ 6assoc\ 5/a\ 6 //]
+qed.
\ No newline at end of file