Proofgold Proposition

∀ x0 x1 . x1 ∈ x0 ⟶ x0 = binunion (setminus x0 (Sing x1)) (Sing x1)

type
prop

theory
HotG

name
-

proof
PUXp3..

Megalodon
binunion_remove1_eq

proofgold address
TMUYm..^{binunion_remove1_eq}

creator
14944 Pr4zB../ee1fb..

owner
14944 Pr4zB../ee1fb..

term root
20fce..