Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_f82d0f217e1b2a36bc273d145ee21e9b9e753d654bb0c650cc08860c1b4bd1f0 with
x0,
x1,
atleastp x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x2 of type ι → ι be given.
Apply unknownprop_db24d9aa1dc52b3c0eaf7cf69655226164a8ab5afc5d72e14a32016133f537ca with
x0,
x1,
x2,
atleastp x0 x1 leaving 2 subgoals.
The subproof is completed by applying H1.
Assume H3:
∀ x3 . In x3 x1 ⟶ ∃ x4 . and (In x4 x0) (x2 x4 = x3).
Apply unknownprop_195b1896e39adea3e4c323b2af14ecdeb2c1304596ebe1419779cc28787a8a2b with
x0,
x1,
x2.
The subproof is completed by applying H2.