proposition: Lemma modulus_q_productive_q: forall xi alpha beta (h:emits_q xi alpha beta), let xi':=fstT (sndT (modulus_q xi alpha beta h)) in let alpha':=fstT (sndT (sndT (modulus_q xi alpha beta h))) in let beta':=sndT (sndT (sndT (modulus_q xi alpha beta h))) in productive_q xi alpha beta -> productive_q xi' alpha' beta'.
proof: Proof. intros xi alpha beta h xi' alpha' beta' h_p_alpha_beta. constructor. intro n. inversion h_p_alpha_beta. generalize (H (S n)). subst xi'. subst alpha'. subst beta'. apply step_productive_q_S_inv_2. Defined.
imports: digits