| pf |
|---|
Apply set_ext with 23e07.. (4ae4a.. 4a7ef..), 4ae4a.. 4a7ef.. leaving 2 subgoals.
Let x0 of type ι be given.
Apply unknownprop_eac7a6683c5ba7aa6ad74545e4a4f065634321e5b116001d3b7a7c41d91b1bf6 with 4ae4a.. 4a7ef.., x0, prim1 x0 (4ae4a.. 4a7ef..) leaving 3 subgoals.
The subproof is completed by applying unknownprop_3d71b8748f06c73392acc73d46c8ae7fc07e5709a18169240b1cb765b8547148.
The subproof is completed by applying H0.
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with 4ae4a.. 4a7ef.., λ x1 x2 . prim1 (e4431.. x0) x2 ⟶ 099f3.. x0 (4ae4a.. 4a7ef..) ⟶ prim1 x0 (4ae4a.. 4a7ef..) leaving 2 subgoals.
Apply unknownprop_67a9b4da3479f0b3ecc9f46f5080b801e2df28e772a8a9215f9b75577fbd1e20 with 4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_70a9111fbca1264eee8cb9291eadf4d76112dae5d2986289cdc9631de7adb2fc.
Apply unknownprop_c3102c186c7aa1001a5c1b1b7ecab6b25bcd639e713104221ece8bf414726a69 with 4a7ef.., x0 leaving 4 subgoals.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
The subproof is completed by applying H1.
Apply unknownprop_514ace28c9a90c94edf6ffd2272d2d1fb4fe92ef818112b7c45dc1e893a67196 with λ x1 x2 . x2 = e4431.. x0.
Apply unknownprop_459e83445e8fa8de123fbedd463b0dc265e95a234964864b65a5d4287e2775ea with e4431.. x0, λ x1 . 4a7ef.. = x1 leaving 2 subgoals.
The subproof is completed by applying H2.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H4.
Apply unknownprop_514ace28c9a90c94edf6ffd2272d2d1fb4fe92ef818112b7c45dc1e893a67196 with λ x1 x2 . SNoEq_ x2 4a7ef.. x0.
Apply SNoEq_I with 4a7ef.., 4a7ef.., x0.
Let x1 of type ι be given.
Apply FalseE with iff (prim1 x1 4a7ef..) (prim1 x1 x0).
Apply unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x1.
The subproof is completed by applying H4.
Apply L4 with λ x1 x2 . prim1 x1 (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
Let x0 of type ι be given.
Apply unknownprop_459e83445e8fa8de123fbedd463b0dc265e95a234964864b65a5d4287e2775ea with x0, λ x1 . prim1 x1 (23e07.. (4ae4a.. 4a7ef..)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ecae2d2d3708015d34ac3eacd84df17c3571bd5e56ae2362f9cb0de5042f4b16 with 4ae4a.. 4a7ef.., 4a7ef.. leaving 4 subgoals.
The subproof is completed by applying unknownprop_3d71b8748f06c73392acc73d46c8ae7fc07e5709a18169240b1cb765b8547148.
The subproof is completed by applying unknownprop_a66a65189a5389c2141d18df52f52fcf5f074fba68040a0bda3b8b81c830611a.
Apply unknownprop_514ace28c9a90c94edf6ffd2272d2d1fb4fe92ef818112b7c45dc1e893a67196 with λ x1 x2 . prim1 x2 (e4431.. (4ae4a.. 4a7ef..)).
Apply unknownprop_b0d5c07b58c35dec2d98b8c0aef5865d54317627a7a2b363b61462669e811c57 with 4ae4a.. 4a7ef.., λ x1 x2 . prim1 4a7ef.. x2 leaving 2 subgoals.
Apply unknownprop_67a9b4da3479f0b3ecc9f46f5080b801e2df28e772a8a9215f9b75577fbd1e20 with 4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_70a9111fbca1264eee8cb9291eadf4d76112dae5d2986289cdc9631de7adb2fc.
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
Apply unknownprop_397dcfaa62ddf41d498e7fd580ff4a854ed9ebd3c9ab727b2b23fe272ecb1aa4 with 4ae4a.. 4a7ef.., 4a7ef.. leaving 2 subgoals.
Apply unknownprop_67a9b4da3479f0b3ecc9f46f5080b801e2df28e772a8a9215f9b75577fbd1e20 with 4ae4a.. 4a7ef...
The subproof is completed by applying unknownprop_70a9111fbca1264eee8cb9291eadf4d76112dae5d2986289cdc9631de7adb2fc.
The subproof is completed by applying unknownprop_375af585d676cd889234cd20860ce45033e1ffceb375ac6277c1b1a2e16f15bd.
■ |
|