Let x0 of type (CT2 (CT2 (ι → ι → ι))) → ι → ι → ι be given.
Assume H0:
∀ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 403c9.. x1 ⟶ fb516.. (x0 x1).
Apply unknownprop_f9b5e20c634bd07d04cdde49271fdc509ca457a000f2db56fe81b30cf7b0806f with
λ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . e7e62.. (λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)),
λ x1 x2 : ο . x2 = ∃ x3 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x3) (6fb7f.. (x0 x3)) leaving 2 subgoals.
The subproof is completed by applying L1.
Apply prop_ext_2 with
∃ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x1) (6fb7f.. (e7e62.. (λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)))),
∃ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x1) (6fb7f.. (x0 x1)) leaving 2 subgoals.
Assume H2:
∃ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x1) (6fb7f.. (e7e62.. (λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)))).
Apply H2 with
∃ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x1) (6fb7f.. (x0 x1)).
Let x1 of type CT2 (ι → ι → ι) be given.
Assume H3:
(λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x2) (6fb7f.. (e7e62.. (λ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x2 x3))))) x1.
Apply H3 with
∃ x2 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x2) (6fb7f.. (x0 x2)).
Claim L5:
∀ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x2 ⟶ fb516.. (x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2))Let x2 of type CT2 (ι → ι → ι) be given.
Apply H0 with
λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2.
Apply and3I with
(λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2) = λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2,
64789.. x1,
64789.. x2 leaving 3 subgoals.
Let x3 of type (CT2 (CT2 (ι → ι → ι))) → (CT2 (CT2 (ι → ι → ι))) → ο be given.
Assume H6: x3 (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2) (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2).
The subproof is completed by applying H6.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
Apply unknownprop_f9b5e20c634bd07d04cdde49271fdc509ca457a000f2db56fe81b30cf7b0806f with
λ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2),
λ x2 x3 : ο . x3 ⟶ ∃ x4 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x4) (6fb7f.. (x0 x4)) leaving 2 subgoals.
The subproof is completed by applying L5.
Assume H6:
∃ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x2) (6fb7f.. (x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2))).
Apply H6 with
∃ x2 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x2) (6fb7f.. (x0 x2)).
Let x2 of type CT2 (ι → ι → ι) be given.
Assume H7:
(λ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x3) (6fb7f.. (x0 (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x3)))) x2.
Apply H7 with
∃ x3 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x3) (6fb7f.. (x0 x3)).
Assume H9:
6fb7f.. (x0 (λ x3 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x3 x1 x2)).
Let x3 of type ο be given.
Assume H10:
∀ x4 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x4) (6fb7f.. (x0 x4)) ⟶ x3.
Apply H10 with
λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2.
Apply andI with
403c9.. (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2),
6fb7f.. (x0 (λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2)) leaving 2 subgoals.
Apply and3I with
(λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2) = λ x4 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x4 x1 x2,
64789.. x1,
64789.. x2 leaving 3 subgoals.
Let x4 of type (CT2 (CT2 (ι → ι → ι))) → (CT2 (CT2 (ι → ι → ι))) → ο be given.
Assume H11: x4 (λ x5 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x5 x1 x2) (λ x5 : (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . x5 x1 x2).
The subproof is completed by applying H11.
The subproof is completed by applying H4.
The subproof is completed by applying H8.
The subproof is completed by applying H9.
Assume H2:
∃ x1 : ((((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → (((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι) → ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (403c9.. x1) (6fb7f.. (x0 x1)).