Proofgold Proposition

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . In x4 x0 ⟶ ∀ x5 . In x5 x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ Repl (setprod x0 x1) (λ x5 . x2 (ap x5 0) (ap x5 1)) = Repl (setprod x0 x1) (λ x5 . x3 (ap x5 0) (ap x5 1))

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
ReplEq_setprod_ext

proofgold address
TMMd6..^{ReplEq_setprod_ext}

creator
1627 PrGxv../3e50b..

owner
1627 PrGxv../3e50b..

term root
366f9..