Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_058b616faa34ba20b642e58766ed0105ac281192cda66dc4064957be4b9ebdfd with
x0,
x1,
x2,
x3,
λ x5 x6 . prim1 x5 (b5c9f.. x4 (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with
4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))),
λ x5 . x4,
λ x5 . 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.
Let x5 of type ι be given.
Apply unknownprop_25845195be761ff55d4782d0bdb7574534fb684dea2c30a90a5fd52c88854f76 with
x5,
λ x6 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (λ x7 . If_i (x7 = 4a7ef..) x0 (If_i (x7 = 4ae4a.. 4a7ef..) x1 (If_i (x7 = 4ae4a.. (4ae4a.. 4a7ef..)) x2 x3)))) x6) x4 leaving 5 subgoals.
The subproof is completed by applying H4.
Apply unknownprop_420bb7efe76e1c91456fb5a55a5e3a5b5429f25f8f9d624532ab60a858f918e6 with
x0,
x1,
x2,
x3,
λ x6 x7 . prim1 x7 x4.
The subproof is completed by applying H0.
Apply unknownprop_a1109e80eebddd03ec86fb5e4a80ba8fed86666bac2429821c4ac4b346fe399a with
x0,
x1,
x2,
x3,
λ x6 x7 . prim1 x7 x4.
The subproof is completed by applying H1.
Apply unknownprop_609acd0443eff633f33b94b7c15d47d918cf33a39d90a74bb85300ccecac83fa with
x0,
x1,
x2,
x3,
λ x6 x7 . prim1 x7 x4.
The subproof is completed by applying H2.
Apply unknownprop_1ebf33d9b27b653d6fc6f75947d3ca0be78ddccf29e0052751261b41f2a90711 with
x0,
x1,
x2,
x3,
λ x6 x7 . prim1 x7 x4.
The subproof is completed by applying H3.