Proofgold Proposition

∀ x0 . In 0 x0 ⟶ ∀ x1 . nat_p x1 ⟶ ∀ x2 . In x2 x1 ⟶ Subq (setexp x0 x2) (setexp x0 x1)

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
nat_in_setexp_mon

proofgold address
TMHBW..^{nat_in_setexp_mon}

creator
1627 PrGxv../4ec08..

owner
1627 PrGxv../4ec08..

term root
de9c7..