proposition: Lemma plus_nf alpha beta : nf alpha -> nf beta -> nf (alpha + beta).
proof: Proof. intros Halpha Hbeta; rewrite <- nf_ref in *; rewrite plus_ref; now apply T1.plus_nf. Qed.
imports: hydras(T1 E0 Comparable) Coq(Arith Logic.Eqdep_dec Peano_dec List Bool Recdef Lia Wellfounded.Inverse_Image Wellfounded.Inclusion RelationClasses )