proposition: Theorem epsilon0_lfp : least_fixpoint lt phi0 epsilon0.
proof: Proof. split. - apply epsilon0_fxp. - intros alpha H; tricho alpha epsilon0 H0. + specialize (lt_phi0 H0); intro H1. rewrite H in H1; destruct (lt_irrefl H1). + subst alpha; now left. + now right. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)