Proofgold Proposition

∀ x0 . x0 ∈ quaternion ⟶ ∀ x1 . x1 ∈ quaternion ⟶ OSNo_proj0 (HSNo_pair x0 x1) = x0

type
prop

theory
HotG

name
octonion_p0_eq

proof
PUcEg..

Megalodon
octonion_p0_eq

proofgold address
TMFKR..^{octonion_p0_eq}

creator
28531 PrQUS../ef78b..

owner
28531 PrQUS../ef78b..

term root
d3193..