def AP.len_app
bend-osdev-array@0.1.0.1 · PROOF.bend:821
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
821def AP.len_app(-T: Data, xs: List<&2, T>, -ys: List<&2, T>) -> {List.length(&2, T, List.append(&2, T, xs, ys)) == Nat.add(List.length(&2, T, xs), List.length(&2, T, ys)) : Nat}:
822 match xs:
823 case Nil{}:
824 {==}
825 case Con{h, t}:
826 AP.succ_cong(List.length(&2, T, List.append(&2, T, t, ys)), Nat.add(List.length(&2, T, t), List.length(&2, T, ys)), AP.len_app(T, t, ys))