(* deleterio per auto? *)
theorem eq_f2: ∀A,B,C.∀f:A→B→C.
∀x1,x2:A.∀y1,y2:B. x1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6x2 → y1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6y2 → f x1 y1 \ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6 f x2 y2.
(* deleterio per auto? *)
theorem eq_f2: ∀A,B,C.∀f:A→B→C.
∀x1,x2:A.∀y1,y2:B. x1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6x2 → y1\ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6y2 → f x1 y1 \ 5A title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/A\ 6 f x2 y2.