#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.
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