proposition: Lemma InA_app_nil_r z l : InA eqA z (l ++ []) ↔ InA eqA z l.
proof: Proof. now rewrite app_nil_r. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.monads