proposition: Lemma formula_eqdec : forall x y : Formula, {x = y} + {x <> y}.
proof: Proof. destruct language_eqdec as [a b]. simple induction x; simple induction y; (right; discriminate) || intros. - induction (term_eqdec t t1) as [a0 | b0]. + induction (term_eqdec t0 t2) as [a1 | b0]. * left; now rewrite a0, a1. * right; unfold not in |- *. intros H. elim b0. inversion H; reflexivity. + right; unfold not in |- *; intros H; elim b0. inversion H; reflexivity. - induction (b r r0) as [a0 | b0]. assert (H: forall (f g : Relations L) (p : f = g) (ts : Terms (arityR L f)) (ss : Terms (arityR L g)) (q : arityR L f = arityR L g), eq_rec _ (fun x => Terms x) ts _ q = ss <-> atomic f ts = atomic g ss). { intros f g p; eapply eq_ind with (x := g) (P := fun a => forall (ts : Terms (arityR L a)) (ss : Terms (arityR L g)) (q : arityR L a = arityR L g), eq_rec _ (fun x => Terms x) ts _ q = ss <-> atomic a ts = atomic g ss). - intros ts ss q; elim q using K_dec_set. + apply eq_nat_dec. + simpl in |- *; split. * intros H; rewrite H; reflexivity. * intros H; inversion H. eapply inj_pair2_eq_dec with (P := fun f : Relations L => Terms (arityR L f)). -- assumption. -- assumption. - auto. } assert (H0: arityR L r = arityR L r0) by (rewrite a0; reflexivity). induction (terms_eqdec _ (eq_rec (arityR L r) (fun x : nat => Terms x) t (arityR L r0) H0) t0) as [a1 | b1]. + left; induction (H _ _ a0 t t0 H0); auto. + right; induction (H _ _ a0 t t0 H0); tauto. + right. intro H; inversion H; auto. - destruct (H f1) as [a0 | b0]. + destruct (H0 f2) as [a1 | b1]. * left; now rewrite a0, a1. * right; intro H3; inversion H3; auto. + right; intro H3; inversion H3; auto. - destruct (H f0) as [e | ne]. + left; now rewrite e. + right; intro H1; inversion H1; auto. - destruct (eq_nat_dec n n0) as [e | ne]. + destruct (H f0) as [a0 | b0]. * left; now rewrite a0, e. * right; intro H1; inversion H1; auto. + right; inversion 1; auto. Qed.
imports: Coq(Lists.List Ensembles Peano_dec Eqdep_dec Arith Compare_dec Utf8) hydras(Ackermann.misc Compat815 )