law range_cons

minebender-game@1.0.0.0 · proof_sums.bend:35

import Base

35# range(1+n) is 0 followed by 1..n.
36law range_cons:
37  for +n: Nat
38  {List.range(1n+n) == 0n <> smap(List.range(n)) : List<&2, Nat>}