Let x0 of type CT2 (ι → ι → ι) be given.
Let x1 of type CT2 (ι → ι → ι) be given.
Apply H0 with
6fb7f.. (cc64c.. (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2))) (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)))) = (x0 = x1).
Assume H2:
and (x0 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ι → ι → ι . x3)) (x0 (λ x3 x4 : ι → ι → ι . x4))) (fb516.. (x0 (λ x2 x3 : ι → ι → ι . x2))).
Apply H2 with
fb516.. (x0 (λ x2 x3 : ι → ι → ι . x3)) ⟶ 6fb7f.. (cc64c.. (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2))) (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)))) = (x0 = x1).
Assume H3: x0 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ι → ι → ι . x3)) (x0 (λ x3 x4 : ι → ι → ι . x4)).
Assume H4:
fb516.. (x0 (λ x2 x3 : ι → ι → ι . x2)).
Assume H5:
fb516.. (x0 (λ x2 x3 : ι → ι → ι . x3)).
Apply H1 with
6fb7f.. (cc64c.. (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2))) (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)))) = (x0 = x1).
Assume H6:
and (x1 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x1 (λ x3 x4 : ι → ι → ι . x3)) (x1 (λ x3 x4 : ι → ι → ι . x4))) (fb516.. (x1 (λ x2 x3 : ι → ι → ι . x2))).
Apply H6 with
fb516.. (x1 (λ x2 x3 : ι → ι → ι . x3)) ⟶ 6fb7f.. (cc64c.. (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2))) (355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)))) = (x0 = x1).
Assume H7: x1 = λ x2 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x2 (x1 (λ x3 x4 : ι → ι → ι . x3)) (x1 (λ x3 x4 : ι → ι → ι . x4)).
Assume H8:
fb516.. (x1 (λ x2 x3 : ι → ι → ι . x2)).
Assume H9:
fb516.. (x1 (λ x2 x3 : ι → ι → ι . x3)).
Apply unknownprop_6891c2c4cbe5dbf32677e09d76954ef64727a2786342d5026c3517fb0288e38a with
355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2)),
355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)),
λ x2 x3 : ο . x3 = (x0 = x1) leaving 3 subgoals.
The subproof is completed by applying L10.
The subproof is completed by applying L11.
Apply unknownprop_3d0028a2d57af707e8620119bacd670d298048a922bcb35db3d1b174e76468c4 with
x0 (λ x2 x3 : ι → ι → ι . x2),
x1 (λ x2 x3 : ι → ι → ι . x2),
λ x2 x3 : ο . and x3 (6fb7f.. (355fd.. (x0 (λ x4 x5 : ι → ι → ι . x5)) (x1 (λ x4 x5 : ι → ι → ι . x5)))) = (x0 = x1) leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply unknownprop_3d0028a2d57af707e8620119bacd670d298048a922bcb35db3d1b174e76468c4 with
x0 (λ x2 x3 : ι → ι → ι . x3),
x1 (λ x2 x3 : ι → ι → ι . x3),
λ x2 x3 : ο . and (x0 (λ x4 x5 : ι → ι → ι . x4) = x1 (λ x4 x5 : ι → ι → ι . x4)) x3 = (x0 = x1) leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H9.
Apply prop_ext_2 with
and (x0 (λ x2 x3 : ι → ι → ι . x2) = x1 (λ x2 x3 : ι → ι → ι . x2)) (x0 (λ x2 x3 : ι → ι → ι . x3) = x1 (λ x2 x3 : ι → ι → ι . x3)),
x0 = x1 leaving 2 subgoals.
Assume H12:
and (x0 (λ x2 x3 : ι → ι → ι . x2) = x1 (λ x2 x3 : ι → ι → ι . x2)) (x0 (λ x2 x3 : ι → ι → ι . x3) = x1 (λ x2 x3 : ι → ι → ι . x3)).
Apply H12 with
x0 = x1.
Assume H13: x0 ... = ....