Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Apply In_rec_i_eq with
λ x3 . λ x4 : ι → ι . If_i (prim1 (prim3 x3) x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0,
4ae4a.. x2,
λ x3 x4 . x4 = x1 x2 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim1 (prim3 x5) x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying nat_primrec_r with x0, x1.
Apply unknownprop_dbe4275ea307e180afd2e52157383232f2331626219d11c06e4e2ea66d247d8d with
x2,
λ x3 x4 . If_i (prim1 x4 (4ae4a.. x2)) (x1 x4 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim1 (prim3 x5) x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x4)) x0 = x1 x2 (In_rec_i (λ x5 . λ x6 : ι → ι . If_i (prim1 (prim3 x5) x5) (x1 (prim3 x5) (x6 (prim3 x5))) x0) x2) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply If_i_1 with
prim1 x2 (4ae4a.. x2),
x1 x2 (In_rec_i (λ x3 . λ x4 : ι → ι . If_i (prim1 (prim3 x3) x3) (x1 (prim3 x3) (x4 (prim3 x3))) x0) x2),
x0.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x2.