proposition: Lemma incl_hd_same {A : Type} (a : A) (l1 l2 : seq A) : incl l1 l2 -> incl (a :: l1) (a :: l2).
proof: Proof. intros Hin. firstorder. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)