proposition: Lemma conc_eq l1 l2 l3 l4 : l1 =i l2 -> l3 =i l4 -> conc l1 l3 =i conc l2 l4.
proof: Proof. move => H1 H2 w. apply: eq_existsb => n. by rewrite (_ : l1 =1 l2) // (_ : l3 =1 l4). Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)