Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: x1 ⊆ x0.
Apply and3I with
struct_b (pack_b {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))),
struct_b (pack_b {x2 ∈ setexp x0 x0|and (bij x0 x0 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))),
unpack_b_o (pack_b {x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)} (λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)))) (λ x2 . λ x3 : ι → ι → ι . unpack_b_o (pack_b {x4 ∈ setexp x0 x0|and (bij x0 x0 (λ x5 . ap x4 x5)) (∀ x5 . x5 ∈ x1 ⟶ ap x4 x5 = x5)} (λ x4 x5 . lam x0 (λ x6 . ap x5 (ap x4 x6)))) (λ x4 . λ x5 : ι → ι → ι . and (and (pack_b {x6 ∈ setexp x0 x0|and (bij x0 x0 (λ x7 . ap x6 x7)) (∀ x7 . x7 ∈ x1 ⟶ ap x6 x7 = x7)} (λ x6 x7 . lam x0 (λ x8 . ap x7 (ap x6 x8))) = pack_b x4 x3) (Group (pack_b x4 x3))) (x4 ⊆ x2))) leaving 3 subgoals.
Apply pack_struct_b_I with
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)).
The subproof is completed by applying unknownprop_8c28017e57ab2ec2cae7456a68ed4001fbd633ee80009212ac3e7002fe0a637a with x0.
Apply pack_struct_b_I with
{x2 ∈ setexp x0 x0|and (bij x0 x0 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)).
Apply unknownprop_84ca4ed305d5b4e27ce2e93e41baee1fcbe8346e3121687514bb4244ad3fd62a with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_673480a732b2360ba263db6ccd7aafefdf5ff6442062595c967c01560edd61e8 with
{x2 ∈ setexp x0 x0|and (bij x0 x0 (λ x3 . ap x2 x3)) (∀ x3 . x3 ∈ x1 ⟶ ap x2 x3 = x3)},
{x2 ∈ setexp x0 x0|bij x0 x0 (λ x3 . ap x2 x3)},
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)),
λ x2 x3 . lam x0 (λ x4 . ap x3 (ap x2 x4)),
λ x2 x3 : ο . x3.