proposition: Lemma case_Eq : alpha + beta = mult_Sn (AP._phi0 a) (S (n + p)) + d.
proof: Proof. unfold alpha, beta; subst c; rewrite <- plus_assoc. rewrite (plus_assoc b (mult_Sn (AP._phi0 a) p) d). rewrite (plus_alpha_mult_phi0 _ _ Hnfa). rewrite plus_assoc; f_equal. rewrite Nat.add_comm; now rewrite mult_Sn_dist. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)