proposition: Lemma subTermExch (t : Term) (v1 v2 : nat) (s1 s2 : Term): v1 <> v2 -> ~ In v2 (freeVarT s1) -> ~ In v1 (freeVarT s2) -> substT (substT t v1 s1) v2 s2 = substT (substT t v2 s2) v1 s1.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => v1 <> v2 -> ~ In v2 (freeVarT s1) -> ~ In v1 (freeVarT s2) -> substTs (substTs ts v1 s1) v2 s2 = substTs (substTs ts v2 s2) v1 s1). - intros n H H0 H1; simpl; induction (eq_nat_dec v1 n) as [a | ?]. + induction (eq_nat_dec v2 n). * elim H; congruence. * rewrite a; rewrite subTermVar1. rewrite subTermNil; auto. + induction (eq_nat_dec v2 n) as [a| ?]. * rewrite a; rewrite subTermVar1. rewrite subTermNil; auto. * now repeat rewrite subTermVar2. - intros f t0 H H0 H1 H2; simpl; rewrite H; auto. - reflexivity. - intros n t0 H t1 H0 H1 H2 H3; simpl; rewrite H; auto. now rewrite H0. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)