Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_primrec_S with 1, λ x0 x1 . mul_nat 2 x1, 1, λ x0 x1 . x1 = 4 leaving 2 subgoals.
The subproof is completed by applying nat_1.
Apply unknownprop_5858d8b36c7cdaccd2f26eae0cf9cb2cc1dc7fc685e15eee42b07d14732d6e73 with 2, λ x0 x1 . mul_nat 2 x1 = 4.
The subproof is completed by applying unknownprop_74ac8a784913fa4a6f9da3de96c05984e11ff1600ef66d703e49d6ee22ad106d.