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