Let x0 of type ι be given.
Apply unknownprop_e5e2df80485f871d64db3fb7f1a412399ce7964e3a578b5b796bab945938f5f4 with
7cb9a.. x0,
x0 leaving 3 subgoals.
Apply unknownprop_444d13dad52ffb55bc4549e4fe523116bd9bc5de1921cdb78d2754d3f831db87 with
x0,
λ x1 x2 . prim1 (e4431.. x0) x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with
e4431.. x0.
Apply unknownprop_fc85352e1b964fa3a21d320d6c72a14a3c5cf7e35a9b3837c2a5de6d8a273717 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_9584d4694d24396c18343b1c0cff3cc590961705df3875e09f245da82f431bce with
x0.
The subproof is completed by applying H0.