proposition: Lemma list_remove_list_submseteq l1 l2 : l1 ⊆+ l2 ↔ is_Some (list_remove_list l1 l2).
proof: Proof. split. - revert l2. induction l1 as [|x l1 IH]; simpl. { intros l2 _. by exists l2. } intros l2. rewrite submseteq_cons_l. intros (k&Hk&?). destruct (list_remove_Some_inv l2 k x) as (k2&?&Hk2); trivial. simplify_option_eq. apply IH. by rewrite <-Hk2. - intros [k Hk]. revert l2 k Hk. induction l1 as [|x l1 IH]; simpl; intros l2 k. { intros. apply submseteq_nil_l. } destruct (list_remove x l2) as [k'|] eqn:?; intros; simplify_eq. rewrite submseteq_cons_l. eauto using list_remove_Some. Qed.
imports: stdpp(options)