Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_primrec_S with 1, λ x0 x1 . mul_nat 2 x1, 2, λ x0 x1 . x1 = 8 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply unknownprop_c2aa62c368a47ae018ac0952ff3137b0b6dc17b9b871ce9eb89fc53a8a9f308f with λ x0 x1 . mul_nat 2 x1 = 8.
The subproof is completed by applying unknownprop_82b4ca10eb7ca03c2ab8db9622e8ff501b1df3632d9b511d2313d8304ef45b38.