law take_append_of_le_length

bend-mathlib@0.8.1.0 · list.bend:1141

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

1141# Taking at most the length of the first part of an append only sees the first part.
1142law take_append_of_le_length:
1143  for -a: Quant
1144  for -A: Kind(a)
1145  for xs: List<a, A>
1146  for ys: List<a, A>
1147  for n: Nat
1148  for h: MNat.le(n, List.length(a, A, xs))
1149  {List.take(a, A, List.append(a, A, xs, ys), n) == List.take(a, A, xs, n) : List<a, A>}