def AP.take_app
bend-osdev-array@0.1.0.1 · PROOF.bend:1379
import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base
1379def AP.take_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.take(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == xs : List<&2, T>}:
1380 match xs:
1381 case Nil{}:
1382 match ys:
1383 case Nil{}:
1384 {==}
1385 case Con{y, t}:
1386 {==}
1387 case Con{x, t}:
1388 AP.con_cong(T, x, List.take(&2, T, List.append(&2, T, t, ys), List.length(&2, T, t)), t, AP.take_app(T, t, ys))