proposition: Lemma re_imageP e v : reflect (image h (re_lang e) v) (v \in re_image e).
proof: Proof. Proof using h_hom. elim: e v => [||a|e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2] v /=. - rewrite inE; constructor. move => [u]. by case. - rewrite inE; apply: (iffP eqP) => [-> |[w] [] /eqP -> <-]; last exact: h0. exists [::]; by rewrite ?h0. - rewrite StringE. apply: (iffP eqP) => [->|[w /=]]. + exists [::a] => //. by rewrite /atom inE. + by rewrite /atom inE => [[]] /eqP -> <-. - apply: (iffP idP) => [/starP [vv] /allP Hvv dev_v|]. have {IHe} Hvv v' : v' \in vv -> image h (re_lang e) v'. by move => /Hvv /= /andP [_ /IHe]. subst v. elim: vv Hvv => [|v vv IHvv] Hvv /=; first by exists [::]; rewrite ?h0. case: (Hvv v (mem_head _ _)) => w [Hw1 Hw2]. case/forall_cons: Hvv => Hv /IHvv [ww [Hww1 Hww2]]. exists (w++ww); split; by [exact: star_cat | rewrite h_hom Hw2 Hww2]. + case => w [] /starP [ww] /allP Hww1 -> <-. rewrite h_flatten //. apply: starI => v' /mapP [w' /Hww1 /= /andP [_ Hw' ->]]. apply/IHe. by exists w'. - apply: (iffP orP). + case => [/IHe1 | /IHe2] [w] [] H <-. exists w => //. by rewrite /plus inE (_ : w \in re_lang e1). exists w => //. by rewrite /plus inE (_ : w \in re_lang e2) ?orbT. + case => w []. case/orP => H <-; [left; apply/IHe1 |right; apply/IHe2]; by exists w. - apply: (iffP idP). + case/concP => v1 [v2] [e] [/IHe1 [w [Hw1 Hw2]] /IHe2 [w' [Hw1' Hw2']]]. exists (w++w'); split; first exact: conc_cat. by rewrite h_hom e Hw2 Hw2'. + case => w [] /concP [w1] [w2] [-> [H1 H2 <-]]. rewrite h_hom. apply: conc_cat; [apply/IHe1|apply/IHe2]. by exists w1. by exists w2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(setoid_leq misc languages dfa nfa)