proposition: Lemma lincl_sim : forall (A:eqType) (eqA: grel A) (hE: Equivalence eqA) (hdec: forall x y, {eqA x y}+{~eqA x y}), forall (l l':seq A), lincl l l' -> r_subset eqA l l'.
proof: Proof. move => A eqA hE hdec l l' hl. apply/(@R_elim _ _ hE hdec). elim : l l' hl => [ | hd tl hi] l' //=. case/andP => hhd htl x. case: (hdec x hd) => //=. move => heq _. rewrite (InA_eq hdec l' heq). by apply: lincl_mem_sim. move => _ hin. by apply: hi. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)