Let x0 of type CT2 (CT2 (ι → ι → ι)) be given.
Let x1 of type CT2 (CT2 (ι → ι → ι)) be given.
Apply H0 with
fb516.. (86a98.. 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)) ⟶ fb516.. (86a98.. 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
fb516.. (86a98.. 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)) ⟶ fb516.. (86a98.. 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_1becf59e2b0a0d9ff1e1505a7a603dfecdbed9318a6b70349a05c972b5872736 with
2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2)),
2a987.. (x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) (x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3)) leaving 2 subgoals.
Apply unknownprop_0c06dd5d44b144394d6a3ddd7a8663f6d933e9c472f59f1dc1655edf63ac023d with
x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2),
x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x2) leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
Apply unknownprop_0c06dd5d44b144394d6a3ddd7a8663f6d933e9c472f59f1dc1655edf63ac023d with
x0 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3),
x1 (λ x2 x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3) leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H9.