From c68f6ae61227544df47512b14e1a74d270dfbb6d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 2 Feb 2010 18:50:29 +0000 Subject: [PATCH] Added Streicher's K axiom. --- helm/software/matita/nlibrary/logic/destruct_bb.ma | 1 + helm/software/matita/nlibrary/logic/equality.ma | 2 ++ 2 files changed, 3 insertions(+) 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 -- 2.39.2