proposition: Lemma InA_app_ass z l₁ l₂ l₃ : InA eqA z (l₁ ++ (l₂ ++ l₃)) ↔ InA eqA z ((l₁ ++ l₂) ++ l₃).
proof: Proof. now rewrite app_ass. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads