Let x0 of type ο be given.
Apply H0 with
56103.. (λ x1 . x1).
Apply andI with
707bb.. 8ac9a.. (56103.. (λ x1 . x1)),
∀ x1 . d701e.. (de327.. 8ac9a.. x1) (57d6a.. (56103.. (λ x2 . x2)) x1) x1 leaving 2 subgoals.
The subproof is completed by applying unknownprop_1f3a0106f649be276c3d554710e20eb930f5b8e542cb4a3cb1f55e6ac6b65fd8 with
8ac9a...
Let x1 of type ι be given.
Apply unknownprop_b6c97af357f42cc10318f5aa27572a1e097448540dfdb447e971d5408a5f51d2 with
de327.. 8ac9a.. x1,
λ x2 . x2,
x1 leaving 2 subgoals.
Let x2 of type ι be given.
Apply unknownprop_97cd06c26cc6b1274a544bade30e933631c1992e032574c4fe030a3cab228183 with
de327.. (de327.. 8ac9a.. x1) x2,
x2.
The subproof is completed by applying unknownprop_8d6cc1e368ee396f68b51d3338711391f5208d276bde615adf4b4d34a28891f9 with
de327.. 8ac9a.. x1,
x2.
Apply unknownprop_97cd06c26cc6b1274a544bade30e933631c1992e032574c4fe030a3cab228183 with
de327.. 8ac9a.. x1,
x1.
The subproof is completed by applying unknownprop_8d6cc1e368ee396f68b51d3338711391f5208d276bde615adf4b4d34a28891f9 with
8ac9a..,
x1.