proposition: Lemma LNN2LNT_subTerms (n : nat) (ts : fol.Terms LNN n) (v : nat) (s : fol.Term LNN): LNN2LNT_terms n (substTs ts v s) = substTs (LNN2LNT_terms n ts) v (LNN2LNT_term s).
proof: Proof. induction ts as [| n t ts Hrects]. - reflexivity. - simpl; now rewrite Hrects, LNN2LNT_subTerm. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)