def internal_length_zero

bend-mathlib@0.8.1.0 · sort.bend:175

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

175def internal_length_zero(~A: Data, +xs: List<&2, A>, e: {List.length(&2, A, xs) == 0n : Nat}) -> {xs == Nil{} : List<&2, A>}:
176  match xs:
177    case Nil{}:
178      {==}
179    case +x <> +t:
180      Empty.absurd({x <> t == Nil{} : List<&2, A>}, MNat.zero_ne_succ(List.length(&2, A, t), Equal.sym(Nat, List.length(&2, A, x <> t), 0n, e)))