proposition: Lemma subAllTermsId (n : nat) (ts : fol.Terms L n): subAllTerms n ts (fun x : nat => var x) = ts.
proof: Proof. induction ts as [| n t ts Hrects]. - reflexivity. - simpl; now rewrite Hrects, subAllTermId. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)