proposition: Lemma modulus_h_PI:forall mu alpha H1 H2, modulus_h mu alpha H1 = modulus_h mu alpha H2.
proof: Proof. intros mu alpha H1. pattern alpha, H1; elim H1 using emits_h_ind_dep; clear H1 mu; [ intros mu alpha0 i H2; generalize i | intros mu alpha0 i H2; generalize i | intros mu alpha0 i H2; generalize i | intros mu alpha0 f H H2; generalize f H ]; pattern alpha0, H2; elim H2 using emits_h_ind_dep; first [ intros mu0 alpha' H_primity H_primity'; simpl; case (Incl_M_dec_D mu0 LL); intro; trivial; contradiction | intros mu0 alpha' H_primity H_primity'; simpl; case (Incl_M_dec_D mu0 RR); intro; trivial; contradiction | intros mu0 alpha' H_primity H_primity'; simpl; case (Incl_M_dec_D mu0 MM); intro; trivial; contradiction | intros; contradiction] || (intro mu0; intros; simpl; case (Incl_M_dec_D mu0 LL); intro; contradiction || case (Incl_M_dec_D mu0 RR); intro; contradiction || case (Incl_M_dec_D mu0 MM); intro; contradiction || trivial). Defined.
imports: digits