def length_append

bend-collections-laws-math@1.0.0.0 · proofs/lib/list.bend:25

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

25def length_append(-A: Data, +xs: List<&2, A>, +ys: List<&2, A>) -> {SC.length(A, SC.append(A, xs, ys)) == Nat.add(SC.length(A, xs), SC.length(A, ys)) : Nat}:
26  match xs:
27    case Nil{}:
28      {==}
29    case Con{+h, +t}:
30      N.succ_cong(SC.length(A, SC.append(A, t, ys)), Nat.add(SC.length(A, t), SC.length(A, ys)), length_append(A, t, ys))