Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Claim L0:
∀ x2 : ι → ι → ο . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ iff (x1 x3 x4) (x2 x3 x4)) ⟶ (λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x2 = (λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x1Let x2 of type ι → ι → ο be given.
Assume H0:
∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ iff (x1 x3 x4) (x2 x3 x4).
Apply prop_ext_2 with
(λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x2,
(λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x1 leaving 2 subgoals.
Assume H1:
(λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x2.
Apply H1 with
(λ x3 . λ x4 : ι → ι → ο . and (∀ x5 . x5 ∈ x3 ⟶ not (x4 x5 x5)) (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ⟶ x4 x6 x5)) x0 x1.
Assume H2:
∀ x3 . x3 ∈ x0 ⟶ not (x2 x3 x3).
Assume H3: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 x4 ⟶ x2 x4 x3.
Apply andI with
∀ x3 . x3 ∈ x0 ⟶ not (x1 x3 x3),
∀ x3 . x3 ∈ ... ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 ⟶ x1 x4 x3 leaving 2 subgoals.
Apply unpack_r_o_eq with
λ x2 . λ x3 : ι → ι → ο . and (∀ x4 . x4 ∈ x2 ⟶ not (x3 x4 x4)) (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 . x5 ∈ x2 ⟶ x3 x4 x5 ⟶ x3 x5 x4),
x0,
x1.
The subproof is completed by applying L0.