~/jendhub

def internal_last_go_append_singleton

bend-mathlib@0.8.1.0 · list.bend:1770

import bend-mathlib@0.8.1.0/list.bend as List
import Base

1770def internal_last_go_append_singleton(a, -A: Kind(a), ys: List<a, A>, -h: A, -x: A) -> {List.last.go(a, A, List.append(a, A, ys, [x]), h) == x : A}:
1771  match ys:
1772    case Nil{}:
1773      {==}
1774    case y <> t:
1775      internal_last_go_append_singleton(a, A, t, y, x)

Uses (3)

Used by (1)