Proofgold Proposition

bij = λ x1 x2 . λ x3 : ι → ι . and (inj x1 x2 x3) (∀ x4 . In x4 x2 ⟶ ∃ x5 . and (In x5 x1) (x3 x5 = x4))

type
prop

theory
hf axiom

name
-

proof
-

Megalodon
bij_def

proofgold address
-

creator

owner

term root
12e58..