From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Tue, 2 Feb 2010 18:50:29 +0000 (+0000)
Subject: Added Streicher's K axiom.
X-Git-Tag: make_still_working~3072
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c68f6ae61227544df47512b14e1a74d270dfbb6d;hp=870b9b017da98021d9163bf45efe9c27b40bb33d;p=helm.git

Added Streicher's K axiom.
---

diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma
index 269cfc765..308f8bebe 100644
--- a/helm/software/matita/nlibrary/logic/destruct_bb.ma
+++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma
@@ -19,6 +19,7 @@ ninductive unit: Type[0] ≝ k: unit.
 ninductive bool: unit → Type[0] ≝ true : bool k | false : bool k.
 
 nlemma foo: true = false → False. #H; ndestruct;
+nqed.
 
 (* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
                ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma
index 6fdac61b9..8ae1bcde4 100644
--- 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