law get_cons_succ

bend-mathlib@0.8.1.0 · list.bend:1703

import Base

1703# The element at index n + 1 of a cons is the element at index n of its tail.
1704law get_cons_succ:
1705  for -a: Quant
1706  for -A: Kind(a)
1707  for -x: A
1708  for -xs: List<a, A>
1709  for -n: Nat
1710  {List.get(a, A, x <> xs, 1n+n) == List.get(a, A, xs, n) : Maybe<a, A>}