Apply unknownprop_f4ee121fb14a7412699d1f11bebf17d33e1718030f72ebf91211f8d97c32541d with
λ x0 . 09364.. x0 = 4ae4a.. x0.
Let x0 of type ι be given.
Apply set_ext with
09364.. x0,
4ae4a.. x0 leaving 2 subgoals.
Let x1 of type ι be given.
Apply unknownprop_b16c51a027be568304bbf4d10214f2f7bab4a7ef1f3929990ec85447bbbf7c12 with
x0,
x1,
prim1 x1 (4ae4a.. x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply H3 with
λ x2 x3 . prim1 x3 (4ae4a.. x0).
Apply unknownprop_7e0c935491619684fa66567f06da9cc071afa3d37e60afae747b20bc8c762543 with
x0.
The subproof is completed by applying H0.
Apply exandE_i with
λ x2 . prim1 x2 x0,
λ x2 . x1 = 09364.. x2,
prim1 x1 (4ae4a.. x0) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x2 of type ι be given.
Apply H5 with
λ x3 x4 . prim1 x4 (4ae4a.. x0).
Apply H1 with
x2,
λ x3 x4 . prim1 x4 (4ae4a.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_ce7857b9839b8f7083d025f6387f2962c755c06bcc9de82bcdf74f1839394154 with
x0,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H4.
Let x1 of type ι be given.
Apply unknownprop_dec2978c0a72cebd51fcab0a380f03d4d80d1ccd8f826d378953148c305a60f0 with
x0,
x1,
prim1 x1 (09364.. x0) leaving 3 subgoals.
The subproof is completed by applying H2.
Apply unknownprop_aca6b7de025ab03c50b497c9de8f58254c0701f6ade5e0855cf800060b35ff63 with
x1,
prim1 x1 (09364.. x0) leaving 3 subgoals.
Apply unknownprop_e6223cc37d124575a1439a62a8bd81090d2105429a9944c39d898ad59aaee24d with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
Apply H4 with
λ x2 x3 . prim1 x3 (09364.. x0).
The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.
Apply exandE_i with
ba9d8..,
λ x2 . x1 = 4ae4a.. x2,
prim1 x1 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply H6 with
λ x3 x4 . prim1 x4 (09364.. x0).
Apply H6 with
λ x3 x4 . prim1 x2 x4.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x2.
Apply unknownprop_43b9163da17f2f66e991f3dd23439608e22bc07ac3880a089612020a7b3f5243 with
x0,
x1,
x2 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L7.
Apply H1 with
x2,
λ x3 x4 . prim1 x3 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying L8.
Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with
x0,
x2.
The subproof is completed by applying L8.
Assume H3: x1 = x0.
Apply H3 with
λ x2 x3 . prim1 x3 (09364.. x0).
Apply unknownprop_aca6b7de025ab03c50b497c9de8f58254c0701f6ade5e0855cf800060b35ff63 with
x0,
prim1 x0 (09364.. x0) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply H4 with
λ x2 x3 . prim1 x3 (09364.. x0).
The subproof is completed by applying unknownprop_f2280590a4843dd3047de5e5151d043be723c7f73a981e4edcbfbfe0904566e7 with x0.
Apply exandE_i with
ba9d8..,
λ x2 . x0 = 4ae4a.. x2,
prim1 x0 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying H4.
Let x2 of type ι be given.
Apply H6 with
λ x3 x4 . prim1 x4 (09364.. x0).
Apply H1 with
x2,
λ x3 x4 . prim1 x3 (09364.. x0) leaving 2 subgoals.
The subproof is completed by applying L7.
Apply unknownprop_83de80e22aba688e4d8cf3ccc9ec372406ae5110cef0bf0846317bfd1d974b00 with
...,
....
Let x0 of type ι be given.
Apply unknownprop_497ceb2eb28aaf14c46cc38f218092e3e652567d5b5313af58a8c57d6bddfd1b with
x0,
λ x1 x2 . x2 = 4ae4a.. x0.
Apply L0 with
x0.
The subproof is completed by applying H1.