proposition: Theorem inject_of_omega : inject T1omega = Schutte_basics._omega.
proof: Proof. simpl; repeat rewrite alpha_plus_zero. rewrite phi0_zero; generalize omega_second_AP; destruct 1. red in H; unfold Ensembles.In in H0; now rewrite omega_eqn. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)