-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
-
+axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
\ No newline at end of file