-ndefinition R0 ≝ λT:Type[0].λt:T.t.
-
-ndefinition R1 ≝ eq_rect_Type0.
-
-ndefinition R2 :
- ∀T0:Type[0].
- ∀a0:T0.
- ∀T1:∀x0:T0. a0=x0 → Type[0].
- ∀a1:T1 a0 (refl_eq ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
- ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
- ∀b0:T0.
- ∀e0:a0 = b0.
- ∀b1: T1 b0 e0.
- ∀e1:R1 ?? T1 a1 ? e0 = b1.
- T2 b0 e0 b1 e1.
- #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
- napply (eq_rect_Type0 ????? e1);
- napply (R1 ?? ? ?? e0);
- napply a2;
-nqed.
-
-ndefinition R3 :
- ∀T0:Type[0].
- ∀a0:T0.
- ∀T1:∀x0:T0. a0=x0 → Type[0].
- ∀a1:T1 a0 (refl_eq ? a0).
- ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
- ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
- ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
- ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
- ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
- ∀b0:T0.
- ∀e0:a0 = b0.
- ∀b1: T1 b0 e0.
- ∀e1:R1 ?? T1 a1 ? e0 = b1.
- ∀b2: T2 b0 e0 b1 e1.
- ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
- T3 b0 e0 b1 e1 b2 e2.
- #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
- napply (eq_rect_Type0 ????? e2);
- napply (R2 ?? ? ???? e0 ? e1);
- napply a3;
-nqed.
-
-ndefinition R4 :
- ∀T0:Type[0].
- ∀a0:T0.
- ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
- ∀a1:T1 a0 (refl_eq 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_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq 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_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
- a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq 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.
- Type[0].
- ∀a4:T4 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
- a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2)
- a3 (refl_eq (T3 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)
- a2 (refl_eq (T2 a0 (refl_eq T0 a0) a1 (refl_eq (T1 a0 (refl_eq T0 a0)) a1)) a2))
- a3).
- ∀b0:T0.
- ∀e0:eq (T0 …) a0 b0.
- ∀b1: T1 b0 e0.
- ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
- ∀b2: T2 b0 e0 b1 e1.
- ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
- ∀b3: T3 b0 e0 b1 e1 b2 e2.
- ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
- T4 b0 e0 b1 e1 b2 e2 b3 e3.
- #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
- napply (eq_rect_Type0 ????? e3);
- napply (R3 ????????? e0 ? e1 ? e2);
- napply a4;
-nqed.
-
-nlemma symmetric_neq : ∀T:Type.∀x,y:T.x ≠ y → y ≠ x.