Proofgold Proposition

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 . x2 ∈ SNoL (mul_SNo x0 x1) ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ SNoL x0 ⟶ ∀ x5 . x5 ∈ SNoL x1 ⟶ SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ x3) ⟶ (∀ x4 . x4 ∈ SNoR x0 ⟶ ∀ x5 . x5 ∈ SNoR x1 ⟶ SNoLe (add_SNo x2 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ x3) ⟶ x3

type
prop

theory
HotG

name
mul_SNo_SNoL_interpolate_impred

proof
PUYBq..

Megalodon
mul_SNo_SNoL_interpolate_impred

proofgold address
TMUjL..^{mul_SNo_SNoL_interpolate_impred}

creator
5053 Pr6Pc../a11b2..

owner
5053 Pr6Pc../a11b2..

term root
395b7..