Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_f32d4fee0581bd88650842cb1ad1dcead0ace674ce79df201ac5743fec6d1273 with
x0,
x1,
x2,
λ x4 x5 . prim1 x4 (b5c9f.. x3 (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))).
Apply unknownprop_78f4273a7b4d13f02d77d194b65be481121674fd021f4ffb88d69be4bcd0ab71 with
4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)),
λ x4 . x3,
λ x4 . f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x5 . If_i (x5 = 4a7ef..) x0 (If_i (x5 = 4ae4a.. 4a7ef..) x1 x2))) x4.
Let x4 of type ι be given.
Apply unknownprop_f024220e6a7fff8a2204de6e8c772bd07090549a0c3549d8f07dd4ceeec2f7f0 with
x4,
λ x5 . prim1 (f482f.. (0fc90.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))) (λ x6 . If_i (x6 = 4a7ef..) x0 (If_i (x6 = 4ae4a.. 4a7ef..) x1 x2))) x5) x3 leaving 4 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_c6edfe304716447202fa4e847b9eb9d6f1ad651728e21f6781503da40cd9117f with
x0,
x1,
x2,
λ x5 x6 . prim1 x6 x3.
The subproof is completed by applying H0.
Apply unknownprop_d7d39a6ae9dd573b529ad4d558553a3d5dfa88cfa249f628a74ae5b338307a3e with
x0,
x1,
x2,
λ x5 x6 . prim1 x6 x3.
The subproof is completed by applying H1.
Apply unknownprop_7a16b690fe761b47a98a266409f7c10953d45924d4b6dee50c46a27a0cf018bb with
x0,
x1,
x2,
λ x5 x6 . prim1 x6 x3.
The subproof is completed by applying H2.