Let x0 of type ι be given.
Apply unknownprop_30912f2cca40a10142321c491284d8399f9fb6058ea49ef0a3ac5fa1be4efa52 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_ea78574cb3264467ecb0cee6dab0f2cbbdf0e0a00f843238d57e1be6acdbe25f with
5246e.. x0.
Let x1 of type ι be given.
Apply unknownprop_9139ee2a8df08ed3f37f7756be409060ff2feed4e0a070067f7d01230efaf1e9 with
x0,
x1,
prim1 x1 4a7ef.. leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H3.
Apply L2 with
λ x2 x3 . prim1 (e4431.. x1) x3 ⟶ 099f3.. x0 x1 ⟶ prim1 x1 4a7ef...
Apply FalseE with
prim1 x1 4a7ef...
Apply unknownprop_86d1ac064e08bd36bc8f8c7d3070ea65b389686b3ca603e510b47119b9d626ec with
x1.
Apply unknownprop_fb545b225a42993d98e0d062b6c9208b8321e87814f4e26de3418c134068c2c8 with
x1,
x0,
x1 leaving 5 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L1.
The subproof is completed by applying H4.
Apply unknownprop_6987e7564cf46ad4d313ff96c864cc87566281cc7f9f5613cde1c6af34a43fdb with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
The subproof is completed by applying H6.