proposition: Lemma subSubTerm (t : Term) (v1 v2 : nat) (s1 s2 : Term): v1 <> v2 -> ~ In v1 (freeVarT s2) -> substT (substT t v1 s1) v2 s2 = substT (substT t v2 s2) v1 (substT s1 v2 s2).
proof: Proof. intros H H0. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => substTs (substTs ts v1 s1) v2 s2 = substTs (substTs ts v2 s2) v1 (substT s1 v2 s2)); simpl in |- *. - intros n. destruct (eq_nat_dec v1 n) as [ e | n0]. + destruct (eq_nat_dec v2 n) as [e0 | n0]. * elim H; transitivity n; auto. * simpl in |- *; destruct (eq_nat_dec v1 n)as [e0 | n1]. -- reflexivity. -- elim n1;auto. + simpl in |- *; destruct (eq_nat_dec v2 n) as [e | n1]. * rewrite subTermNil; easy. * simpl in |- *; destruct (eq_nat_dec v1 n) as [e | ]. -- elim n0; auto. -- reflexivity. - intros f t0 H1; rewrite H1; reflexivity. - reflexivity. - intros n t0 H1 t1 H2; rewrite H1, H2; easy. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(ListExt folProp folProof folLogic subProp folReplace)