Proofgold Proposition

∀ x0 x1 x2 x3 x4 x5 x6 x7 . (∀ x8 . x8 ∈ x6 ⟶ ∀ x9 : ο . (∀ x10 . x10 ∈ x2 ⟶ ∀ x11 . x11 ∈ x3 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ (∀ x10 . x10 ∈ x4 ⟶ ∀ x11 . x11 ∈ x5 ⟶ x8 = add_SNo (mul_SNo x10 x1) (add_SNo (mul_SNo x0 x11) (minus_SNo (mul_SNo x10 x11))) ⟶ x9) ⟶ x9) ⟶ (∀ x8 . x8 ∈ x2 ⟶ ∀ x9 . x9 ∈ x3 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7) ⟶ (∀ x8 . x8 ∈ x4 ⟶ ∀ x9 . x9 ∈ x5 ⟶ add_SNo (mul_SNo x8 x1) (add_SNo (mul_SNo x0 x9) (minus_SNo (mul_SNo x8 x9))) ∈ x7) ⟶ x6 ⊆ x7

type
prop

theory
HotG

name
mul_SNo_Subq_lem

proof
PUU9n..

Megalodon
mul_SNo_Subq_lem

proofgold address
TMVJd..^{mul_SNo_Subq_lem}

creator
4981 Pr6Pc../f106e..

owner
4981 Pr6Pc../f106e..

term root
cc834..