proposition: Lemma homographic_absorbs :forall mu alpha (p:productive_h mu alpha), ~(Incl_M mu LL)->~(Incl_M mu RR)->~(Incl_M mu MM)-> forall p', bisim (homographic mu alpha p) (homographic (product mu (hd alpha)) (tl alpha) p').
proof: Proof. intros mu alpha p t_l t_r t_m p'. rewrite homographic_unfolded. rewrite (homographic_unfolded (product mu (hd alpha))). generalize (productive_h_emits_h _ _ p); intros t. generalize (modulus_h_absorbs _ _ t t_l t_r t_m (emits_h_absorbs_inv _ _ t_l t_r t_m t)). intros H_eq. generalize (modulus_h_productive_h mu alpha t p). rewrite H_eq. rewrite (modulus_h_PI _ _ (emits_h_absorbs_inv mu alpha t_l t_r t_m t) (productive_h_emits_h (product mu (hd alpha)) (tl alpha) p')). constructor; simpl; trivial; apply homographic_EPI. Defined.
imports: digits