Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: subgroup x0 x1.

Let x2 of type ι → ι → ο be given.

Assume H1: ∀ x3 x4 . ∀ x5 : ι → ι → ι . (∀ x6 . x6 ∈ x4 ⟶ ∀ x7 . x7 ∈ x4 ⟶ x5 x6 x7 ∈ x4) ⟶ Group (pack_b x3 x5) ⟶ x3 ⊆ x4 ⟶ x2 (pack_b x3 x5) (pack_b x4 x5).

Apply H0 with x2 x0 x1.

Assume H2: and (struct_b x1) (struct_b x0).

Assume H3: unpack_b_o x1 (λ x3 . λ x4 : ι → ι → ι . unpack_b_o x0 (λ x5 . λ x6 : ι → ι → ι . and (and (x0 = pack_b x5 x4) (Group (pack_b x5 x4))) (x5 ⊆ x3))).

Apply H2 with x2 x0 x1.

Assume H4: struct_b x1.

Assume H5: struct_b x0.

Claim L6: subgroup x0 x1 ⟶ x2 x0 x1

Apply H4 with λ x3 . subgroup x0 x3 ⟶ x2 x0 x3.

Let x3 of type ι be given.

Let x4 of type ι → ι → ι be given.

Assume H6: ∀ x5 . x5 ∈ x3 ⟶ ∀ x6 . x6 ∈ x3 ⟶ x4 x5 x6 ∈ x3.

Apply H5 with λ x5 . subgroup x5 (pack_b x3 x4) ⟶ x2 x5 (pack_b x3 x4).

Let x5 of type ι be given.

Let x6 of type ι → ι → ι be given.

Assume H7: ∀ x7 . x7 ∈ x5 ⟶ ∀ x8 . x8 ∈ x5 ⟶ x6 x7 x8 ∈ x5.

Assume H8: subgroup (pack_b x5 x6) (pack_b x3 x4).

Apply pack_b_subgroup_E with x5, x3, x6, x4, x2 (pack_b x5 x6) (pack_b x3 x4) leaving 2 subgoals.

The subproof is completed by applying H8.

Assume H9: pack_b x5 x6 = pack_b x5 x4.

Assume H10: explicit_subgroup x3 x4 x5.

Apply H10 with x2 (pack_b x5 x6) (pack_b x3 x4).

Assume H11: Group (pack_b x5 x4).

Assume H12: x5 ⊆ x3.

Apply H9 with λ x7 x8 . x2 x8 (pack_b x3 x4).

Apply H1 with x5, x3, x4 leaving 3 subgoals.

The subproof is completed by applying H6.

The subproof is completed by applying H11.

The subproof is completed by applying H12.

Apply L6.

The subproof is completed by applying H0.

■

Proofgold Proof