-napply (eq_rect_Type0 ????? e3);
-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
- | napply refl
- | #x; #y; #H; nrewrite < H; napply refl
- | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
-nqed.
-
-naxiom T1 : Type[0].
-naxiom T2 : T1 → Type[0].
-naxiom t1 : T1.
-naxiom t2 : ∀x:T1. T2 x.
-
-ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝
+apply (eq_rect_Type0 ????? e3);
+apply (R3 ????????? e0 ? e1 ? e2);
+apply a4;
+qed.
+
+axiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
+
+definition EQ: ∀A:Type[0]. equivalence_relation A.
+ #A; apply mk_equivalence_relation
+ [ apply eq
+ | apply refl
+ | #x; #y; #H; rewrite < H; apply refl
+ | #x; #y; #z; #Hyx; #Hxz; rewrite < Hxz; assumption]
+qed.
+
+axiom T1 : Type[0].
+axiom T2 : T1 → Type[0].
+axiom t1 : T1.
+axiom t2 : ∀x:T1. T2 x.
+
+inductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝