Let x0 of type (CT2 (ι → ι → ι)) → ι → ι → ι be given.
Assume H0:
∀ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . 64789.. x1 ⟶ fb516.. (x0 x1).
Apply unknownprop_f0cbad33a378e3e85280c199dc1e363589ab8e9ee5da068efeebef66c30d2dc6 with
λ x1 : ι → ι → ι . 0f571.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)),
λ x1 x2 : ο . x2 = ∃ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x3) (6fb7f.. (x0 x3)) leaving 2 subgoals.
The subproof is completed by applying L1.
Apply prop_ext_2 with
∃ x1 : ι → ι → ι . and (fb516.. x1) (6fb7f.. (0f571.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)))),
∃ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x1) (6fb7f.. (x0 x1)) leaving 2 subgoals.
Assume H2:
∃ x1 : ι → ι → ι . and (fb516.. x1) (6fb7f.. (0f571.. (λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)))).
Apply H2 with
∃ x1 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x1) (6fb7f.. (x0 x1)).
Let x1 of type ι → ι → ι be given.
Assume H3:
(λ x2 : ι → ι → ι . and (fb516.. x2) (6fb7f.. (0f571.. (λ x3 : ι → ι → ι . x0 (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x2 x3))))) x1.
Apply H3 with
∃ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x2) (6fb7f.. (x0 x2)).
Claim L5:
∀ x2 : ι → ι → ι . fb516.. x2 ⟶ fb516.. (x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2))Let x2 of type ι → ι → ι be given.
Apply H0 with
λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2.
Apply and3I with
(λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2) = λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2,
fb516.. x1,
fb516.. x2 leaving 3 subgoals.
Let x3 of type (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_f0cbad33a378e3e85280c199dc1e363589ab8e9ee5da068efeebef66c30d2dc6 with
λ x2 : ι → ι → ι . x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2),
λ x2 x3 : ο . x3 ⟶ ∃ x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x4) (6fb7f.. (x0 x4)) leaving 2 subgoals.
The subproof is completed by applying L5.
Assume H6:
∃ x2 : ι → ι → ι . and (fb516.. x2) (6fb7f.. (x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2))).
Apply H6 with
∃ x2 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x2) (6fb7f.. (x0 x2)).
Let x2 of type ι → ι → ι be given.
Assume H7:
(λ x3 : ι → ι → ι . and (fb516.. x3) (6fb7f.. (x0 (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x3)))) x2.
Apply H7 with
∃ x3 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x3) (6fb7f.. (x0 x3)).
Assume H9:
6fb7f.. (x0 (λ x3 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x3 x1 x2)).
Let x3 of type ο be given.
Assume H10:
∀ x4 : ((ι → ι → ι) → (ι → ι → ι) → ι → ι → ι) → ι → ι → ι . and (64789.. x4) (6fb7f.. (x0 x4)) ⟶ x3.
Apply H10 with
λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2.
Apply andI with
64789.. (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2),
6fb7f.. (x0 (λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2)) leaving 2 subgoals.
Apply and3I with
(λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2) = λ x4 : (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι . x4 x1 x2,
fb516.. x1,
fb516.. x2 leaving 3 subgoals.
Let x4 of type (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 (64789.. x1) (6fb7f.. (x0 x1)).