proposition: Lemma lminus_incl : forall l1 l2, sim_incl l2 (l1 ++ (lminus l2 l1)).
proof: Proof. move => l1; elim => [ | hd tl] //=. case_eq (InA l1 hd) => /=. - move => hIn ->. by rewrite InA_cat hIn. - move => hIn. move/sim_inclP. move/R_elim => hincl. case_eq (sim_incl tl (l1 ++ hd :: lminus tl l1)) => /=. + move => _. rewrite InA_cat. by rewrite InA_hd orbT. + case/sim_inclP. apply/R_elim => x0 hx0. move : (hincl x0 hx0). rewrite !InA_cat /=. case/orP => -> //=. by case: eqA_dec => /= ; rewrite orbT. Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)