Proofgold Proposition

∀ x0 x1 . ∀ x2 x3 : ι → ι → ι . (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x1 ⟶ x2 x4 x5 = x3 x4 x5) ⟶ {x2 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1} = {x3 (ap x5 0) (ap x5 1)|x5 ∈ setprod x0 x1}

type
prop

theory
HotG

name
ReplEq_setprod_ext

proof
PUgbQ..

Megalodon
ReplEq_setprod_ext

proofgold address
TMTDN..^{ReplEq_setprod_ext}

creator
4904 Pr6Pc../c116b..

owner
4904 Pr6Pc../c116b..

term root
c486a..