law take_append_of_le_length_sym

bend-mathlib@0.8.1.0 · list.bend:2597

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

2597# Taking at most the length of the first part of an append only sees the first part, reversed to rewrite toward the simple side.
2598law take_append_of_le_length_sym:
2599  for -a: Quant
2600  for -A: Kind(a)
2601  for xs: List<a, A>
2602  for ys: List<a, A>
2603  for n: Nat
2604  for h: MNat.le(n, List.length(a, A, xs))
2605  {List.take(a, A, xs, n) == List.take(a, A, List.append(a, A, xs, ys), n) : List<a, A>}