proposition: Lemma suffix_lookup_Some l1 l2 i x : l1 !! i = Some x → l1 `suffix_of` l2 → l2 !! (i + (length l2 - length l1)) = Some x.
proof: Proof. intros. by rewrite <-suffix_lookup_lt by eauto using lookup_lt_Some. Qed.
imports: stdpp(options)