Let x0 of type ι → ο be given.

Assume H0: ∀ x1 . x0 x1 ⟶ struct_e x1.

Claim L1: ∀ x1 x2 x3 . x0 x1 ⟶ x0 x2 ⟶ PtdSetHom x1 x2 x3 ⟶ x3 ∈ setexp (ap x2 0) (ap x1 0)

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Assume H1: x0 x1.

Assume H2: x0 x2.

Apply H0 with x1, λ x4 . PtdSetHom x4 x2 x3 ⟶ x3 ∈ setexp (ap x2 0) (ap x4 0) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x4 of type ι be given.

Let x5 of type ι be given.

Assume H3: x5 ∈ x4.

Apply H0 with x2, λ x6 . PtdSetHom (pack_e x4 x5) x6 x3 ⟶ x3 ∈ setexp (ap x6 0) (ap (pack_e x4 x5) 0) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H4: x7 ∈ x6.

Apply unknownprop_266cf3934e79ff708b43f6101066886a004a8b2cb57b38750ae943dbc174c7c9 with x4, x6, x5, x7, x3, λ x8 x9 : ο . x9 ⟶ x3 ∈ setexp (ap (pack_e x6 x7) 0) (ap (pack_e x4 x5) 0).

Assume H5: and (x3 ∈ setexp x6 x4) (ap x3 x5 = x7).

Apply pack_e_0_eq2 with x6, x7, λ x8 x9 . x3 ∈ setexp x8 (ap (pack_e x4 x5) 0).

Apply pack_e_0_eq2 with x4, x5, λ x8 x9 . x3 ∈ setexp x6 x8.

Apply H5 with x3 ∈ setexp x6 x4.

Assume H6: x3 ∈ setexp x6 x4.

Assume H7: ap x3 x5 = x7.

The subproof is completed by applying H6.

Apply unknownprop_cb7abf829499aec888363ff9292dd7680786c42dc92f10fdd88dc16ada048723 with x0, λ x1 . ap x1 0, PtdSetHom.

The subproof is completed by applying L1.

■

Proofgold Proof