proposition: Lemma subTermVar2 : forall (v x : nat) (s : fol.Term L), v <> x -> substT (var x) v s = var x.
proof: Proof. intros v x s H; unfold substT in |- *. destruct (eq_nat_dec v x); [contradiction | reflexivity]. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)