proposition: Lemma L_R (X : seq A) x y : L^[set z in X] x y =i R^X x y.
proof: Proof. elim: X x y => [|z X' IH] x y w. - rewrite (_ : [set z in [::]] = set0) //=. apply/idP/mem_R0. + move/L_set0 => [[-> ->]|[a -> ->]]; by eauto. + move => [[-> ->]|[a -> <-]]; apply/LP => /=; split => // [[|i]] //. - rewrite set_cons /= (L_rec _ _) -2!topredE /= /plus /= IH. f_equal. apply: conc_eq; first exact: IH. apply: conc_eq; last exact: IH. apply: star_eq. exact: IH. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)