law get_cons_succ_sym

bend-mathlib@0.8.1.0 · list.bend:2924

import Base

2924# The element at index n + 1 of a cons is the element at index n of its tail, reversed to rewrite toward the simple side.
2925law get_cons_succ_sym:
2926  for -a: Quant
2927  for -A: Kind(a)
2928  for -x: A
2929  for -xs: List<a, A>
2930  for -n: Nat
2931  {List.get(a, A, xs, n) == List.get(a, A, x <> xs, 1n+n) : Maybe<a, A>}