proposition: Lemma InA_permute_heads z x y l : InA eqA z (x :: y :: l) → InA eqA z (y :: x :: l).
proof: Proof. intros E1. inversion_clear E1 as [|?? E2]; auto. inversion_clear E2; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads