Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_7963a4bf2feda239add5cf25163811bc2206f6f21a0e4a70277699970e74fa1e with
x1,
x2,
atleastp x0 x2 leaving 2 subgoals.
The subproof is completed by applying H1.
Let x3 of type ι → ι be given.
Apply unknownprop_6a8f953ba7c3bf327e583b76a91b24ddd499843a498fbfe2514e26f3800e68b3 with
x1,
x2,
x3,
atleastp x0 x2 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H3:
∀ x4 . In x4 x1 ⟶ In (x3 x4) x2.
Assume H4:
∀ x4 . In x4 x1 ⟶ ∀ x5 . In x5 x1 ⟶ x3 x4 = x3 x5 ⟶ x4 = x5.
Claim L5:
∀ x4 . In x4 x0 ⟶ In x4 x1Apply unknownprop_cc8f63ddfbec05087d89028647ba2c7b89da93a15671b61ba228d6841bbab5e9 with
x0,
x1.
The subproof is completed by applying H0.
Apply unknownprop_195b1896e39adea3e4c323b2af14ecdeb2c1304596ebe1419779cc28787a8a2b with
x0,
x2,
x3.
Apply unknownprop_57c8600e4bc6abecef2ae17962906fa2de1fc16f5d46ed100ff99cd5b67f5b1b with
x0,
x2,
x3 leaving 2 subgoals.
Let x4 of type ι be given.
Apply H3 with
x4.
Apply L5 with
x4.
The subproof is completed by applying H6.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H4 with
x4,
x5 leaving 2 subgoals.
Apply L5 with
x4.
The subproof is completed by applying H6.
Apply L5 with
x5.
The subproof is completed by applying H7.