Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: equip x0 x1.
Apply H0 with atleastp x0 x1.
Let x2 of type ιι be given.
Assume H1: bij x0 x1 x2.
Let x3 of type ο be given.
Assume H2: ∀ x4 : ι → ι . inj x0 x1 x4x3.
Apply H2 with x2.
Apply bij_inj with x0, x1, x2.
The subproof is completed by applying H1.