proposition: Lemma nf_epsilon : forall alpha, nf alpha -> nf (epsilon alpha).
proof: Proof. compute; auto with T2. Qed.
imports: Coq(Arith Compare_dec Relations Wellfounded Lia) hydras(More_Arith Restriction T1 OrdNotations Compat815)