~/jendhub

def AP.drop_app

bend-osdev-array@0.1.0.1 · PROOF.bend:1390

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF
import Base

1390def AP.drop_app(-T: Data, xs: List<&2, T>, ys: List<&2, T>) -> {List.drop(&2, T, List.append(&2, T, xs, ys), List.length(&2, T, xs)) == ys : List<&2, T>}:
1391  match xs:
1392    case Nil{}:
1393      match ys:
1394        case Nil{}:
1395          {==}
1396        case Con{y, t}:
1397          {==}
1398    case Con{x, t}:
1399      AP.drop_app(T, t, ys)

Uses (4)

Used by (1)