proposition: Lemma subTermNil (t : Term) (v : nat) (s : Term): ~ In v (freeVarT t) -> substT t v s = t.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => ~ In v (freeVarTs ts) -> substTs ts v s = ts). - intros n H; simpl in H; rewrite subTermVar2. + reflexivity. + intro H0; apply H; left; auto. - intros f t0 H H0; simpl; rewrite H. + reflexivity. + apply H0. - reflexivity. - intros n t0 H t1 H0 H1; simpl; unfold freeVarTs in H1. rewrite H0. + rewrite H. * reflexivity. * intros H2; elim H1; apply in_or_app. auto. + intro H2; elim H1; apply in_or_app; now right. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)