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 (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0, 4a7ef.., λ x2 x3 . x3 = x0 leaving 2 subgoals.
The subproof is completed by applying nat_primrec_r with x0, x1.
Apply If_i_0 with prim1 (prim3 4a7ef..) 4a7ef.., x1 (prim3 4a7ef..) (In_rec_i (λ x2 . λ x3 : ι → ι . If_i (prim1 (prim3 x2) x2) (x1 (prim3 x2) (x3 (prim3 x2))) x0) (prim3 4a7ef..)), x0.
The subproof is completed by applying unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with prim3 4a7ef...