proposition: Lemma depth_h_PI_strong:forall mu mu' alpha alpha' H1 H2, mu=mu'->alpha=alpha' -> depth_h mu alpha H1 = depth_h mu' alpha' H2.
proof: Proof. intros; subst; apply depth_h_PI. Defined.
imports: digits Refining_M homographic Streams_addenda RIneq QArithSternBrocot(R_addenda) rep