X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPlogic%2Fequality.ma;h=a5972e2709446cce6a401ba28c228e93920b54ac;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=68e7aa50917fae4e68e80d702b8bb89a3a035350;hpb=08281577f00c9d178ff3227b49ab96e600917998;p=helm.git

diff --git a/helm/software/matita/nlibrary/Plogic/equality.ma b/helm/software/matita/nlibrary/Plogic/equality.ma
index 68e7aa509..a5972e270 100644
--- 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