proposition: Lemma incl_switch_head' {A} (x : A) (y l r : list A) : incl r (x :: y ++ l) -> incl r (y ++ x :: l).
proof: Proof. unfold incl in *. intuition. specialize (H a H0). simpl in *; rewrite -> in_app_iff in *. simpl in *. intuition auto. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect