def gapp_nil

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:232

import Base

232def gapp_nil(-A: Data, +xs: List<&2, A>) -> {xs == List.append(&2, A, xs, Nil{}) : List<&2, A>}:
233  match xs:
234    case Nil{}:
235      {==}
236    case Con{h, t}:
237      %gapp_nil(A, t) : {Con{h, t} == Con{h, _} : List<&2, A>}
238      {==}