proposition: Lemma plus_nf : forall alpha, nf alpha -> forall beta, nf beta -> nf (alpha + beta).
proof: Proof. intros alpha Halpha; pattern alpha; apply transfinite_induction; trivial. - destruct x. + cbn;auto with T2. + destruct beta. * cbn;auto with T2. * intros; cbn; case_eq ( compare (gcons x1 x2 0 zero) (gcons beta1 beta2 0 zero)). -- intro;apply nf_intro. ++ nf_inv. ++ nf_inv. ++ generalize ( compare_Eq H2); injection 1. intros; subst beta1; subst beta2; inversion_clear H1. auto with T2. apply psi_lt_head;auto with T2. ++ nf_inv. -- auto. -- intro;apply nf_intro. ++ nf_inv. ++ nf_inv. ++ apply psi_principal. nf_inv. ** inversion H;auto with T2. apply psi_lt_head;auto with T2. ** apply psi_lt_head;unfold psi; apply compare_Gt;auto with T2. ++ eapply H0;auto with T2. ** nf_inv. ** apply lt_tail;auto with T2. Qed.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)