proposition: Lemma suffix_lookup_lt l1 l2 i : i < length l1 → l1 `suffix_of` l2 → l1 !! i = l2 !! (i + (length l2 - length l1)).
proof: Proof. intros Hi [k ->]. rewrite app_length, lookup_app_r by lia. f_equal; lia. Qed.
imports: stdpp(options)