Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ιιι be given.
Apply In_rec_i_eq with λ x2 . λ x3 : ι → ι . If_i (prim3 x2x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0, 0, λ x2 x3 . x3 = x0 leaving 2 subgoals.
The subproof is completed by applying nat_primrec_r with x0, x1.
Apply If_i_0 with prim3 00, x1 (prim3 0) (In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim3 x2x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0) (prim3 0)), x0.
The subproof is completed by applying EmptyE with prim3 0.