proposition: Lemma subTermVar1 : forall (v : nat) (s : fol.Term L), substT (var v) v s = s.
proof: Proof. intros v s; unfold substT in |- *. destruct (eq_nat_dec v v) as [e | b]. - reflexivity. - now destruct b. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)