Commit c1687739 authored by Robbert Krebbers's avatar Robbert Krebbers

Prove elem_of_submseteq.

parent 0144c537
Pipeline #3851 passed with stage
in 5 minutes and 17 seconds
......@@ -1873,6 +1873,10 @@ Proof.
Global Instance: AntiSymm (≡ₚ) (@submseteq A).
Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
Lemma elem_of_submseteq l k x : x ∈ l → l ⊆+ k → x ∈ k.
Proof. intros ? [l' ->]%submseteq_Permutation. apply elem_of_app; auto. Qed.
Lemma submseteq_take l i : take i l ⊆+ l.
Proof. auto using sublist_take, sublist_submseteq. Qed.
Lemma submseteq_drop l i : drop i l ⊆+ l.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment