- ∀T1:∀x0:T0. <A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> T0 a0 x0 → Type[0].
- ∀a1:T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0).
- ∀T2:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1 → Type[0].
- ∀a2:T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1).
- ∀T3:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1.
- ∀x2:T2 x0 p0 x1 p1.<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T2 …) (<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
- ∀a3:T3 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)
- a2 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T2 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0) a1 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> (T1 a0 (<A href="cic:/matita/basics/logic/eq.con(0,1,2)">refl</A> T0 a0)) a1)) a2).
- ∀T4:∀x0:T0. ∀p0:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T1 …) (<A href="cic:/matita/basics/logic/R1.def(2)">R1</A> T0 a0 T1 a1 x0 p0) x1.
- ∀x2:T2 x0 p0 x1 p1.∀p2:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T2 …) (<A href="cic:/matita/basics/logic/R2.def(3)">R2</A> T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
- ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:<A href="cic:/matita/basics/logic/eq.ind(1,0,2)">eq</A> (T3 …) (<A href="cic:/matita/basics/logic/R3.def(4)">R3</A> T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
+ ∀T1:∀x0:T0. \ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 T0 a0 x0 → Type[0].
+ ∀a1:T1 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0).
+ ∀T2:∀x0:T0. ∀p0:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T1 …) (\ 5A href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/A\ 6 T0 a0 T1 a1 x0 p0) x1 → Type[0].
+ ∀a2:T2 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0) a1 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 (T1 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0)) a1).
+ ∀T3:∀x0:T0. ∀p0:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T1 …) (\ 5A href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/A\ 6 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T2 …) (\ 5A href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/A\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
+ ∀a3:T3 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0) a1 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 (T1 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0)) a1)
+ a2 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 (T2 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0) a1 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 (T1 a0 (\ 5A href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/A\ 6 T0 a0)) a1)) a2).
+ ∀T4:∀x0:T0. ∀p0:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T1 …) (\ 5A href="cic:/matita/basics/logic/R1.def(2)"\ 6R1\ 5/A\ 6 T0 a0 T1 a1 x0 p0) x1.
+ ∀x2:T2 x0 p0 x1 p1.∀p2:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T2 …) (\ 5A href="cic:/matita/basics/logic/R2.def(3)"\ 6R2\ 5/A\ 6 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:\ 5A href="cic:/matita/basics/logic/eq.ind(1,0,2)"\ 6eq\ 5/A\ 6 (T3 …) (\ 5A href="cic:/matita/basics/logic/R3.def(4)"\ 6R3\ 5/A\ 6 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.