Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . prim5 x0 x1 = famunion x0 (λ x3 . Sing (x1 x3))

type
prop

theory
HotG

name
ReplEq_famunion_Sing

proof
PUL8Q..

Megalodon
ReplEq_famunion_Sing

proofgold address
TMbPF..^{ReplEq_famunion_Sing}

creator
4882 Pr6Pc../d1fb8..

owner
4882 Pr6Pc../d1fb8..

term root
dfa22..