X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=261cd77a84ab7770205ef49756dd6ce7f91754e9;hb=2912d9bd61bc451c1135ca0a123cc30f203e93c9;hp=6723cf2cc4bbca3d4a0797d50b8d97c8495d0fb2;hpb=a6602de6db0993a67c5b23aedb3c8fe1d484855f;p=helm.git

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 6723cf2cc..261cd77a8 100644
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -27,6 +27,11 @@ lemma eq_ind_r :
  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
 
+lemma eq_rect_Type0_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+  cases p; //; qed.
+  
 lemma eq_rect_Type2_r:
   ∀A.∀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 (generalize in match H) (generalize in match P)