Commit 2024-04-24 13:42 add5ed22

View on Github →

feat(List): add lemmas about Sublist (#12326)

  • Move tail_sublist to Basic
  • Rename sublist_of_cons_sublist_cons to Sublist.of_cons_cos
  • Rename cons_sublist_cons_iff to cons_sublist_cons
  • Add Sublist.tail, drop_sublist_drop_left, Sublist.drop
  • Protect some lemmas

Estimated changes

added theorem List.tail_sublist
deleted theorem List.tail_sublist