proposition: Lemma InA_comm z l₁ l₂ : InA eqA z (l₁ ++ l₂) → InA eqA z (l₂ ++ l₁).
proof: Proof. rewrite !(InA_app_iff _). tauto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads