proposition: Lemma Permutation_InA2 : forall l l' x, Permutation l l' -> InA2 x l -> InA2 x l'.
proof: Proof. move => l l' x h. move: x. elim : h => //=; clear l l'. - move => x l l' h hi y. case/SetoidList.InA_cons. move => ->. by apply/SetoidList.InA_cons; left; reflexivity. move => h'. apply/SetoidList.InA_cons; right. by apply hi. - move => x y l a. case/SetoidList.InA_cons. move => ->. apply/SetoidList.InA_cons; right. by apply/SetoidList.InA_cons; left; reflexivity. case/SetoidList.InA_cons. move => ->. by apply/SetoidList.InA_cons; left; reflexivity. move => h; apply/SetoidList.InA_cons; right. by apply/SetoidList.InA_cons; right. - move => l1 l2 l3 hperm1 hi1 hperm2 hi2 a hIn. by apply: hi2 ; apply: hi1. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)