proposition: Lemma subAllTermId (t : fol.Term L): subAllTerm t (fun x : nat => var x) = t.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => subAllTerms n ts (fun x : nat => var x) = ts); simpl. - reflexivity. - intros f t0 H; now rewrite H. - reflexivity. - intros n t0 H t1 H0; now rewrite H, H0. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)