proposition: Lemma sim_inclP : forall l l', reflect (r_subset l l') (sim_incl l l').
proof: Proof. move => l l'. apply: (iffP idP). - move => h. apply/R_elim. elim: l l' h => [ | hd tl hi] l' //=. move: (hi l'). case_eq (sim_incl tl l') => hsim //= hnil. move : (hnil (refl_equal true) hd) => //. case_eq (InA l' hd) => heq //= hIn _ x. case: (eqA_dec x hd) => //=. * move => heq2 _. by rewrite (InA_eq l' heq2). * move => _ hin2. by apply: hi. - move/R_elim. elim: l l' => [ | hd tl hi] l' //= h. move: (hi l'). case_eq (sim_incl tl l') => hsim //=. * move => _. apply: h. by apply: InA_hd. * apply => x hx. apply: h. by case: (eqA_dec x hd). Qed.
imports: Coq(RelationClasses Setoid Morphisms SetoidList Mergesort Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegexpBrzozowski(glue)