severe bug found in parallel zeta

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

diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma
index 68e7aa50917fae4e68e80d702b8bb89a3a035350..a5972e2709446cce6a401ba28c228e93920b54ac 100644 (file)
--- a/helm/software/matita/nlibrary/Plogic/equality.ma
+++ b/helm/software/matita/nlibrary/Plogic/equality.ma
@@ -29,6 +29,12 @@ nlemma eq_ind_r :
  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
 nqed.
 
+nlemma eq_rect_Type2_r :
+  ∀A:Type.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A;#a;#P;#H;#x;#p;ngeneralize in match H;ngeneralize in match P;
+  ncases p;//;
+nqed.
+
 (*
 nlemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
@@ -134,4 +140,4 @@ 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.
\ No newline at end of file
+naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
\ No newline at end of file