proposition: Lemma homographic_emits_L :forall mu alpha (p:productive_h mu alpha), (Incl_M mu LL) -> forall p', bisim (homographic mu alpha p) (Cons LL (homographic (product inv_LL mu) alpha p')).
proof: Proof. intros mu alpha p t_l p'. rewrite homographic_unfolded. rewrite (homographic_unfolded (product inv_LL mu)). generalize (productive_h_emits_h _ _ p); intros t. generalize (modulus_h_productive_h mu alpha t p). rewrite (modulus_h_L _ _ t t_l). intros. constructor; simpl; trivial. rewrite <- homographic_unfolded; apply homographic_EPI. Defined.
imports: digits