proposition: Lemma subTermTrans (t : Term) (v1 v2 : nat) (s : Term): ~ In v2 (List.remove eq_nat_dec v1 (freeVarT t)) -> substT (substT t v1 (var v2)) v2 s = substT t v1 s.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => ~ In v2 (List.remove eq_nat_dec v1 (freeVarTs ts)) -> substTs (substTs ts v1 (var v2)) v2 s = substTs ts v1 s). - intros n H; simpl; induction (eq_nat_dec v1 n) as [? | b]. + now rewrite (subTermVar1 L). + rewrite (subTermVar2 L). * reflexivity. * simpl in H; destruct (Nat.eq_dec v1 n). -- elim b; auto. -- intro H0; elim H. simpl; auto. - intros f t0 H H0; simpl; rewrite H. + reflexivity. + apply H0. - auto. - intros n t0 H t1 H0 H1; simpl; unfold freeVarTs in H1. rewrite H0. * rewrite H. -- reflexivity. -- intros H2; elim H1; apply in_in_remove. ++ eapply in_remove_neq, H2. ++ apply in_or_app; left. eapply in_remove, H2. * intro H2; elim H1; apply in_in_remove. -- eapply in_remove_neq, H2. -- apply in_or_app; right; eapply in_remove, H2. Qed.
imports: Coq(Ensembles List Peano_dec) hydras.Ackermann(ListExt) Coq(Arith) hydras.Ackermann(folProof folLogic folProp folReplace)