proposition: Lemma submseteq_length_Permutation l1 l2 : l1 ⊆+ l2 → length l2 ≤ length l1 → l1 ≡ₚ l2.
proof: Proof. intros Hsub Hlen. destruct (submseteq_Permutation l1 l2) as [[|??] Hk]; auto. - by rewrite Hk, (right_id_L [] (++)). - rewrite Hk, app_length in Hlen. simpl in *; lia. Qed.
imports: stdpp(options)