Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . (∀ x2 . x2 ∈ x0 ⟶ x1 (x1 x2) = x2) ⟶ prim5 (prim5 x0 x1) x1 = x0

type
prop

theory
HotG

name
invol_Repl_eq

proof
PUK1b..

Megalodon
invol_Repl_eq

proofgold address
TMW5Y..^{invol_Repl_eq}

creator
4949 Pr6Pc../46e6b..

owner
4949 Pr6Pc../46e6b..

term root
87b06..