proposition: Lemma LNT2LNN_subTerm (t : Term) (v : nat) (s : Term): LNT2LNN_term (substT t v s) = substT (LNT2LNN_term t) v (LNT2LNN_term s).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms LNT n) => LNT2LNN_terms n (substTs ts v s) = substTs (LNT2LNN_terms n ts) v (LNT2LNN_term s)); simpl. - intro n; destruct (eq_nat_dec v n); reflexivity. - intros f t0 H; rewrite H; reflexivity. - reflexivity. - intros n t0 H t1 H0; now rewrite H, H0. Qed.
imports: Coq(Ensembles List Arith) hydras.Ackermann(misc ListExt folProp folProof Languages subAll subProp folLogic3 folReplace LNN LNT codeNatToTerm NewNotations)