law pre_tail

lawful-fields@0.1.1.0 · proof_cut.bend:449

import Base

449law pre_tail:
450  for +xs: List<&2, U32>
451  for +s: Nat
452  for +x: U32
453  for +t: List<&2, U32>
454  for +hp: {List.take(&2, U32, List.drop(&2, U32, xs, s), 1n+List.length(&2, U32, t)) == x <> t : List<&2, U32>}
455  {List.take(&2, U32, List.drop(&2, U32, xs, Nat.add(s, 1n)), List.length(&2, U32, t)) == t : List<&2, U32>}