proposition: Lemma nfb_equiv gamma : nfb gamma = true <-> nf gamma.
proof: Proof. induction gamma. - cbn; split;auto. constructor. - simpl; destruct gamma3; split. + case_eq (nfb gamma1); case_eq (nfb gamma2); try discriminate; rewrite IHgamma1 , IHgamma2; try constructor; auto. + inversion_clear 1; rewrite <- IHgamma1 in H0; rewrite <- IHgamma2 in H1. now rewrite H0, H1. + case_eq (compare [gamma3_1, gamma3_2] [gamma1, gamma2]); intro Hcompare; try discriminate. generalize (compare_Lt Hcompare). constructor; auto. apply andb_prop in H0; destruct H0. apply andb_prop in H1; destruct H1. tauto. apply andb_prop in H0; destruct H0. apply andb_prop in H1; destruct H1. tauto. apply andb_prop in H0; destruct H0. apply andb_prop in H1; destruct H1. tauto. + inversion_clear 1. apply compare_rw_lt in H0. rewrite H0. rewrite <- IHgamma1 in H1; rewrite H1. rewrite <- IHgamma2 in H2; rewrite H2. rewrite <- IHgamma3 in H3; rewrite H3. reflexivity. 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)