proposition: Lemma quadratic_EPI_strong:forall xi xi' alpha alpha' beta beta' p p', xi=xi'->alpha=alpha'->beta=beta'-> bisim (quadratic xi alpha beta p) (quadratic xi' alpha' beta' p').
proof: Proof. cofix. intros; rewrite quadratic_unfolded; rewrite (quadratic_unfolded _ _ _ p'); constructor; simpl; [ idtac | apply quadratic_EPI_strong ]; rewrite (modulus_q_PI_strong _ _ _ _ _ _ (productive_q_emits_q xi alpha beta p) (productive_q_emits_q xi' alpha' beta' p')); trivial. Defined.
imports: digits