Proofgold Proposition

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . subgroup (pack_b x0 x2) (pack_b x1 x3) ⟶ and (pack_b x0 x2 = pack_b x0 x3) (explicit_subgroup x1 x3 x0)

type
prop

theory
HotG

name
pack_b_subgroup_E

proof
PUMaE..

Megalodon
pack_b_subgroup_E

proofgold address
TMaQ7..^{pack_b_subgroup_E}

creator
4924 Pr6Pc../5e4b1..

owner
4924 Pr6Pc../5e4b1..

term root
7125f..