proposition: Theorem embedding : fun_bijection (nf: Ensemble T1) (members epsilon0) inject.
proof: Proof. split. - intros x Hx; apply inject_lt_epsilon0. - intros y Hy; destruct (inject_lt_epsilon0_ex y Hy) as [x [Hx Hx1]]; exists x; auto. - intros x x' Hx Hx' H; apply inject_injective; auto. Qed.
imports: hydras(Epsilon0.Epsilon0 ON_Generic) hydras(Schutte_basics Schutte.Addition AP CNF)