Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . ∀ x3 x4 : ι → ι . (∀ x5 . In x5 x2 ⟶ x3 x5 = x4 x5) ⟶ If_i (In (Union x2) x2) (x1 (Union x2) (x3 (Union x2))) x0 = If_i (In (Union x2) x2) (x1 (Union x2) (x4 (Union x2))) x0

type
prop

theory
HF

name
-

proof
PUVGM..

Megalodon
nat_primrec_r

proofgold address
TMVNd..^{nat_primrec_r}

creator
2277 PrGxv../674ce..

owner
2277 PrGxv../674ce..

term root
e652f..