- ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
- ∀a1:T1 a0 (refl T0 a0).
- ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
- ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
- ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
- ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
- ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
- ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
- ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
- ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 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.