proposition: Lemma homographic_unfolded:forall mu alpha p, homographic mu alpha p = Cons (fstT (modulus_h mu alpha (productive_h_emits_h mu alpha p))) (homographic (fstT(sndT(modulus_h mu alpha (productive_h_emits_h mu alpha p)))) (sndT(sndT(modulus_h mu alpha (productive_h_emits_h mu alpha p)))) (modulus_h_productive_h mu alpha (productive_h_emits_h mu alpha p) p)).
proof: Proof. intros; rewrite (unfold_Stream (homographic mu alpha p)); reflexivity. Defined.
imports: digits