Proofgold Proposition

∀ x0 x1 . ∀ x2 : ι → ι . Subq x0 x1 ⟶ (∀ x3 . In x3 x1 ⟶ nIn x3 x0 ⟶ In 0 (x2 x3)) ⟶ Subq (Pi x0 x2) (Pi x1 x2)

type
prop

theory
HF

name
-

proof
PUKA4..

Megalodon
Pi_0_dom_mon

proofgold address
TMRHp..^Pi_0_dom_mon

creator
1627 PrGxv../5e85f..

owner
1627 PrGxv../5e85f..

term root
81768..