Let x0 of type CT2 (CT2 (ι → ι → ι)) be given.
Let x1 of type CT2 (CT2 (ι → ι → ι)) be given.
Apply H0 with
6fb7f.. (cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)))) = (x0 = x1).
Assume H2:
and (x0 = λ x2 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2 (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x0 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4))) (64789.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))).
Apply H2 with
64789.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) ⟶ 6fb7f.. (cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (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:
64789.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)).
Assume H5:
64789.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)).
Apply H1 with
6fb7f.. (cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)))) = (x0 = x1).
Assume H6:
and (x1 = λ x2 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2 (x1 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x3 x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4))) (64789.. (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))).
Apply H6 with
64789.. (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) ⟶ 6fb7f.. (cc64c.. (2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2))) (2a987.. (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:
64789.. (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)).
Assume H9:
64789.. (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)).
Apply unknownprop_6891c2c4cbe5dbf32677e09d76954ef64727a2786342d5026c3517fb0288e38a with
2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)),
2a987.. (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_2f766ca4fba18e4ffcf2933872105bdd6cbc546146efe808f87254bbe50ed160 with
x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2),
x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2),
λ x2 x3 : ο . and x3 (6fb7f.. (2a987.. (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_2f766ca4fba18e4ffcf2933872105bdd6cbc546146efe808f87254bbe50ed160 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 ... = ....