Proofgold Term Root Disambiguation

λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (∀ x3 : ο . (∀ x4 . and (and (and (and (∀ x5 . x5 ∈ ordsucc x2 ⟶ Group (ap x4 x5)) (∀ x5 . x5 ∈ x2 ⟶ normal_subgroup (ap x4 (ordsucc x5)) (ap x4 x5))) (∀ x5 . x5 ∈ x2 ⟶ abelian_Group (quotient_Group (ap x4 x5) (ap x4 (ordsucc x5))))) (x0 = ap x4 0)) (trivial_Group_p (ap x4 x2)) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1

as obj
da0c1..^{solvable_Group_p}

as prop
-

theory
HotG

stx
6b5ba..

address
TMX5X..^{solvable_Group_p}