Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Claim L0:
∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4) ⟶ (λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x2 = (λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x1Let x2 of type ι → ι → ι be given.
Assume H0: ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x3 x4 = x2 x3 x4.
Apply prop_ext_2 with
(λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) x0 x2,
(λ x3 . λ x4 : ι → ι → ι . and (and (∃ x5 . and (x5 ∈ x3) (∀ x6 . x6 ∈ x3 ⟶ and (x4 x6 x5 = x6) (x4 x5 x6 = x6))) (∀ x5 . x5 ∈ x3 ⟶ bij x3 x3 (λ x6 . x4 x5 x6))) (∀ x5 . ... ∈ ... ⟶ bij x3 x3 (λ x6 . x4 x6 x5))) ... ... leaving 2 subgoals.
Apply unpack_b_o_eq with
λ x2 . λ x3 : ι → ι → ι . and (and (∃ x4 . and (x4 ∈ x2) (∀ x5 . x5 ∈ x2 ⟶ and (x3 x5 x4 = x5) (x3 x4 x5 = x5))) (∀ x4 . x4 ∈ x2 ⟶ bij x2 x2 (λ x5 . x3 x4 x5))) (∀ x4 . x4 ∈ x2 ⟶ bij x2 x2 (λ x5 . x3 x5 x4)),
x0,
x1.
The subproof is completed by applying L0.