def append_nil

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:262

import Base

262def append_nil(+xs: List<&2, Nat>) -> {List.append(&2, Nat, xs, Nil{}) == xs : List<&2, Nat>}:
263  match xs:
264    case Nil{}:
265      {==}
266    case +x <> +rest:
267      Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => x <> tail, List.append(&2, Nat, rest, Nil{}), rest, append_nil(rest))