Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Assume H4: x0 = x1 ⟶ ∀ x4 : ο . x4.
Assume H5: x0 = x2 ⟶ ∀ x4 : ο . x4.
Assume H6: x0 = x3 ⟶ ∀ x4 : ο . x4.
Assume H7: x1 = x2 ⟶ ∀ x4 : ο . x4.
Assume H8: x1 = x3 ⟶ ∀ x4 : ο . x4.
Assume H9: x2 = x3 ⟶ ∀ x4 : ο . x4.
Apply unknownprop_350f82fd4df83c2030aa9fe95c59b3e2660a97bcb0cb01e460d56aaef04b44cb with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))),
λ x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 (If_i (x5 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) x4 leaving 3 subgoals.
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)).
Apply unknownprop_11171438c9340577bc5ca6838eccea0ebdb4279227053bf618ee42741f7851b4 with
4ae4a.. (4ae4a.. 4a7ef..).
The subproof is completed by applying unknownprop_db15d8db2f5eec557f7b3f5a742d4a0a45fde052cadd58f24d03c6c32a463f49.
Let x4 of type ι be given.
Apply unknownprop_25845195be761ff55d4782d0bdb7574534fb684dea2c30a90a5fd52c88854f76 with
x4,
λ x5 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 (If_i (x6 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) leaving 5 subgoals.
The subproof is completed by applying H10.
Apply unknownprop_420bb7efe76e1c91456fb5a55a5e3a5b5429f25f8f9d624532ab60a858f918e6 with
x0,
x1,
x2,
x3,
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
The subproof is completed by applying H0.
Apply unknownprop_a1109e80eebddd03ec86fb5e4a80ba8fed86666bac2429821c4ac4b346fe399a with
x0,
x1,
x2,
x3,
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
The subproof is completed by applying H1.
Apply unknownprop_609acd0443eff633f33b94b7c15d47d918cf33a39d90a74bb85300ccecac83fa with
x0,
x1,
x2,
x3,
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
The subproof is completed by applying H2.
Apply unknownprop_1ebf33d9b27b653d6fc6f75947d3ca0be78ddccf29e0052751261b41f2a90711 with
x0,
x1,
x2,
x3,
λ x5 x6 . prim1 x6 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
The subproof is completed by applying H3.
Let x4 of type ι be given.
Let x5 of type ι be given.