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 set_ext with
23e07.. x0,
56ded.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_eac7a6683c5ba7aa6ad74545e4a4f065634321e5b116001d3b7a7c41d91b1bf6 with
x0,
x1,
prim1 x1 (56ded.. x0) leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H3.
Apply L2 with
λ x2 x3 . prim1 x1 (56ded.. x2).
Apply unknownprop_c00cc223767ee742a69d7b142278ba10f148f15f86cc8e89adc83bb1fda2c95d with
x1,
x0 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying L1.
The subproof is completed by applying H5.
Let x1 of type ι be given.
Apply unknownprop_cd21c13b2c3f5b1a3b98367fcb2ef0b03b319d8c325362ea48d721c1e2e4842f with
x0,
x1,
prim1 x1 (23e07.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying H6.
Apply L2 with
λ x2 x3 . prim1 (e4431.. x1) x3.
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 H6.
The subproof is completed by applying H4.