proposition: Lemma quadratic_emits_L :forall xi alpha beta (p:productive_q xi alpha beta), (Incl_T xi LL) -> forall p', bisim (quadratic xi alpha beta p) (Cons LL (quadratic (m_product inv_LL xi) alpha beta p')).
proof: Proof. intros xi alpha beta p t_l p'. rewrite quadratic_unfolded. rewrite (quadratic_unfolded (m_product inv_LL xi)). generalize (productive_q_emits_q _ _ _ p); intros t. generalize (modulus_q_productive_q xi alpha beta t p). rewrite (modulus_q_L _ _ _ t t_l). intros. constructor; simpl; trivial. rewrite <- quadratic_unfolded; apply quadratic_EPI. Defined.
imports: digits