X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flogic.ma;h=c64f887c6fe0f6b36d90dfebb5a7f2c61897f59e;hb=eac748dd6d912e84b3c78e682f9e40d90fb10acb;hp=5e97f9b5c1bdd4b27da7613edad60fa8c644b917;hpb=7fa016a4bb3d62c4680c02089e21ae0a307af7d0;p=helm.git

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 5e97f9b5c..c64f887c6 100644
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -223,5 +223,4 @@ definition R4 :
 qed.
 
 (* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[2].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p.
-
+axiom streicherK : ∀T:Type[1].∀t:T.∀P:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t → Type[2].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) → ∀p.P p.
\ No newline at end of file