proposition: Lemma subSubAllTerms (n : nat) (ts : fol.Terms L n) (m : nat -> fol.Term L) (v : nat) (s : fol.Term L) : substTs (subAllTerms n ts m) v s = subAllTerms n ts (fun n : nat => substT (m n) v s).
proof: Proof. induction ts as [| n t ts Hrects]. - auto. - simpl; now rewrite subSubAllTerm, Hrects. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)