law cnt1_succ

minebender-game@1.0.0.0 · proof_gen.bend:976

import Base

976law cnt1_succ:
977  for +a: Nat
978  for +xs: List<&2, Nat>
979  {cnt1(1n+a, xs) == cnt(a, xs) : Nat}