proposition: Lemma homographic_EPI_strong:forall mu mu' alpha alpha' p p', mu=mu'->alpha=alpha'-> bisim (homographic mu alpha p) (homographic mu' alpha' p').
proof: Proof. cofix. intros; rewrite homographic_unfolded; rewrite (homographic_unfolded _ _ p'); constructor; simpl ; [ idtac | apply homographic_EPI_strong ]; rewrite (modulus_h_PI_strong _ _ _ _ (productive_h_emits_h mu alpha p) (productive_h_emits_h mu' alpha' p')); trivial. Defined.
imports: digits