proposition: Lemma term_eqdec : forall x y : Term, {x = y} + {x <> y}.
proof: Proof. destruct language_eqdec as [a b]. assert (H: forall (f g : Functions L) (p : f = g) (ts : Terms (arityF L f)) (ss : Terms (arityF L g)) (q : arityF L f = arityF L g), eq_rec _ (fun x => Terms x) ts _ q = ss <-> apply f ts = apply g ss). { intros f g p; eapply eq_ind with (x := g) (P := fun a => forall (ts : Terms (arityF L a)) (ss : Terms (arityF L g)) (q : arityF L a = arityF L g), eq_rec (arityF L a) (fun x : nat => Terms x) ts (arityF L g) q = ss <-> apply a ts = apply g ss). - intros ts ss q; apply K_dec_set with (x := arityF L g) (P := fun z => eq_rec (arityF L g) (fun x : nat => Terms x) ts (arityF L g) z = ss <-> apply g ts = apply g ss). apply eq_nat_dec; simpl in |- *. split. + intros H; rewrite <- H; auto. + intros H; inversion H as [H1]. eapply inj_pair2_eq_dec with (P := fun f : Functions L => Terms (arityF L f)); assumption. - auto. } intro x; elim x using Term_Terms_rec_full with (P0 := fun (n : nat) (ts : Terms n) => forall ss : Terms n, {ts = ss} + {ts <> ss}). intros n y; induction y as [n0| f t]. induction (eq_nat_dec n n0) as [a0 | b0]. + rewrite a0; left; auto. + right; intro H0; inversion H0; contradiction. + right; discriminate. + intros f t H0 y; induction y as [n| f0 t0]. * right; discriminate. * induction (a f f0). assert (H1: arityF L f0 = arityF L f). { rewrite a0. reflexivity. } set (ss' := eq_rec _ (fun z : nat => Terms z) t0 _ H1) in *. assert (H2: f0 = f) by auto. induction (H0 ss'). -- left; induction (H _ _ H2 t0 t H1). symmetry in |- *; apply H3; symmetry in |- *. apply a1. -- right. intros H3. induction (H _ _ H2 t0 t H1) as [H4 H5]. elim b0; symmetry in |- *; apply H5. symmetry in |- *; assumption. -- right. intro H1; inversion H1. contradiction. + left; apply nilTerms. + intros n t H0 t0 H1 ss. induction (consTerms _ ss). induction x0 as (a0, b0); simpl in p. induction (H1 b0) as [a1 | b1]. * induction (H0 a0). -- left; rewrite a1, a2; assumption. -- right; intro H2. elim b1. rewrite <- p in H2; inversion H2; reflexivity. * right; intro H2; elim b1. rewrite <- p in H2; inversion H2. 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 )