Let x0 of type CT2 (ι → ι → ι) be given.
Let x1 of type CT2 (ι → ι → ι) be given.
Apply H0 with
fb516.. (2a987.. 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)) ⟶ fb516.. (2a987.. 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
fb516.. (2a987.. 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)) ⟶ fb516.. (2a987.. 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_1becf59e2b0a0d9ff1e1505a7a603dfecdbed9318a6b70349a05c972b5872736 with
355fd.. (x0 (λ x2 x3 : ι → ι → ι . x2)) (x1 (λ x2 x3 : ι → ι → ι . x2)),
355fd.. (x0 (λ x2 x3 : ι → ι → ι . x3)) (x1 (λ x2 x3 : ι → ι → ι . x3)) leaving 2 subgoals.
Apply unknownprop_79548ff982945a6416517d45c3ad8c5d872f305466e806493afdd4f6a10f88f4 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_79548ff982945a6416517d45c3ad8c5d872f305466e806493afdd4f6a10f88f4 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.