law pow_succ

lawful-arrays@0.1.0.0 · proof_base.bend:229

import Base

229# 2^(1+p) unfolds to p' + (p' + 0); this is p' + p'.
230law pow_succ:
231  for +p: Nat
232  {Nat.pow(2n, 1n+p) == Nat.add(Nat.pow(2n, p), Nat.pow(2n, p)) : Nat}