Proofgold Proposition

∀ x0 : ι → ι → ο . partialorder x0 ⟶ strictpartialorder (λ x1 x2 . and (x0 x1 x2) (x1 = x2 ⟶ ∀ x3 : ο . x3))

type
prop

theory
HotG

name
partialorder_strictpartialorder

proof
PUKtJ..

Megalodon
partialorder_strictpartialorder

proofgold address
TMW6Q..^{partialorder_strictpartialorder}

creator
4890 Pr6Pc../e2530..

owner
4890 Pr6Pc../e2530..

term root
6d855..