Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Assume H3: x0 = x1 ⟶ ∀ x3 : ο . x3.
Assume H4: x0 = x2 ⟶ ∀ x3 : ο . x3.
Assume H5: x1 = x2 ⟶ ∀ x3 : ο . x3.
Apply unknownprop_350f82fd4df83c2030aa9fe95c59b3e2660a97bcb0cb01e460d56aaef04b44cb with
4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)),
λ x3 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x4 . If_i (x4 = 4a7ef..) x0 (If_i (x4 = 4ae4a.. 4a7ef..) x1 x2))) x3 leaving 3 subgoals.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
4ae4a.. (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_db15d8db2f5eec557f7b3f5a742d4a0a45fde052cadd58f24d03c6c32a463f49.
Let x3 of type ι be given.
Apply unknownprop_f024220e6a7fff8a2204de6e8c772bd07090549a0c3549d8f07dd4ceeec2f7f0 with
x3,
λ x4 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 x2))) x4) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) leaving 4 subgoals.
The subproof is completed by applying H6.
Apply unknownprop_c6edfe304716447202fa4e847b9eb9d6f1ad651728e21f6781503da40cd9117f with
x0,
x1,
x2,
λ x4 x5 . prim1 x5 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))).
The subproof is completed by applying H0.
Apply unknownprop_d7d39a6ae9dd573b529ad4d558553a3d5dfa88cfa249f628a74ae5b338307a3e with
x0,
x1,
x2,
λ x4 x5 . prim1 x5 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))).
The subproof is completed by applying H1.
Apply unknownprop_7a16b690fe761b47a98a266409f7c10953d45924d4b6dee50c46a27a0cf018bb with
x0,
x1,
x2,
λ x4 x5 . prim1 x5 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))).
The subproof is completed by applying H2.
Let x3 of type ι be given.
Let x4 of type ι be given.