Proofgold Proposition

∀ x0 x1 . x1 ∈ {x2 ∈ setexp x0 x0|bij x0 x0 (ap x2)} ⟶ explicit_Group_inverse {x3 ∈ setexp x0 x0|bij x0 x0 (ap x3)} (λ x3 x4 . lam x0 (λ x5 . ap x4 (ap x3 x5))) x1 = lam x0 (inv x0 (ap x1))

type
prop

theory
HotG

name
explicit_Group_symgroup_inv_eq

proof
PUMaE..

Megalodon
explicit_Group_symgroup_inv_eq

proofgold address
TMKp3..^{explicit_Group_symgroup_inv_eq}

creator
4924 Pr6Pc../cd167..

owner
4924 Pr6Pc../cd167..

term root
569ca..