proposition: Lemma sublist_cons_l x l k : x :: l `sublist_of` k ↔ ∃ k1 k2, k = k1 ++ x :: k2 ∧ l `sublist_of` k2.
proof: Proof. split. - intros Hlk. induction k as [|y k IH]; inv Hlk. + eexists [], k. by repeat constructor. + destruct IH as (k1&k2&->&?); auto. by exists (y :: k1), k2. - intros (k1&k2&->&?). by apply sublist_inserts_l, sublist_skip. Qed.
imports: stdpp(options)