Proofgold Proposition

∀ x0 . ∀ x1 x2 : ι → ι → ο . x2 x0 (ap (pack_r x0 x1) 0) ⟶ x2 (ap (pack_r x0 x1) 0) x0

type
prop

theory
HotG

name
pack_r_0_eq2

proof
PUSob..

Megalodon
pack_r_0_eq2

proofgold address
TMWSr..^pack_r_0_eq2

creator
4904 Pr6Pc../35a18..

owner
4904 Pr6Pc../35a18..

term root
e9f37..