proposition: Lemma subTermId : forall (t : fol.Term L) (v : nat), substT t v (var v) = t.
proof: Proof. intros ? ?; elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => substTs n ts v (var v) = ts). - simpl in |- *; intros n. induction (eq_nat_dec v n) as [a | b]. + now rewrite a. + reflexivity. - intros f t0 H; simpl in |- *; now rewrite H. - reflexivity. - intros ? ? H t1 H0; simpl in |- *; now rewrite H, H0. Qed.
imports: Coq(Wf_nat Arith Lists.List Peano_dec) hydras.Ackermann(ListExt)