proposition: Lemma InA_app_swap {A} eqA : Equivalence eqA -> forall (a : A) l l', InA eqA a (l ++ l') -> InA eqA a (l' ++ l).
proof: Proof. intros; eapply InA_app_iff; eapply InA_app_iff in H0; eauto; intuition. Qed.
imports: Coq.Sorting.Permutation Fiat.Common Coq.Lists.List Fiat.Common.List.ListFacts Coq.Program.Program Coq.Lists.SetoidList