proposition: Lemma terms_eqdec n (x y : Terms n): {x = y} + {x <> y}.
proof: Proof. induction x as [| n t x Hrecx]. - left; apply nilTerms. - induction (consTerms _ y) as [(a,b) p]. simpl in p. induction (Hrecx b) as [a0 | b0]. + induction (term_eqdec t a) as [a1| b0]. * left; now rewrite a1, a0. * right. intro H; elim b0. rewrite <- p in H. inversion H; reflexivity. + right. intro H; elim b0. rewrite <- p in H. inversion H. eapply inj_pair2_eq_dec with (P := fun n : nat => Terms n). * apply eq_nat_dec. * assumption. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )