Let x0 of type ι be given.

Let x1 of type ι be given.

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

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

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

Apply H0 with and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0).

Assume H1: and (struct_b (pack_b x1 x3)) (struct_b (pack_b x0 x2)).

Apply unknownprop_673480a732b2360ba263db6ccd7aafefdf5ff6442062595c967c01560edd61e8 with x0, x1, x2, x3, λ x4 x5 : ο . x5 ⟶ and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0).

Assume H2: and (and (pack_b x0 x2 = pack_b x0 x3) (Group (pack_b x0 x3))) (x0 ⊆ x1).

Apply H2 with and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0).

Assume H3: and (pack_b x0 x2 = pack_b x0 x3) (Group (pack_b x0 x3)).

Apply H3 with x0 ⊆ x1 ⟶ and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0).

Assume H4: pack_b x0 x2 = pack_b x0 x3.

Assume H5: Group (pack_b x0 x3).

Assume H6: x0 ⊆ x1.

Apply andI with pack_b x0 x2 = pack_b x0 x3, explicit_subgroup x1 x3 x0 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply andI with Group (pack_b x0 x3), x0 ⊆ x1 leaving 2 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H6.

■

Proofgold Proof