Added Streicher's K axiom.

[helm.git] / helm / software / matita / nlibrary / logic / equality.ma

diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 6fdac61b9cf424b4c7ebf2457167d1b959636a9f..8ae1bcde4c0c8640136d3232f2af7ed391726143 100644 (file)
--- a/helm/software/matita/nlibrary/logic/equality.ma
+++ b/helm/software/matita/nlibrary/logic/equality.ma
@@ -117,6 +117,8 @@ napply (R3 ????????? e0 ? e1 ? e2);
 napply a4;
 nqed.
 
+naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. 
+
 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
  #A; napply mk_equivalence_relation
   [ napply eq