proposition: Lemma LNN2LNT_subTerm (t : fol.Term LNN) (v : nat) (s : fol.Term LNN): LNN2LNT_term (substT t v s) = substT (LNN2LNT_term t) v (LNN2LNT_term s).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms LNN n) => LNN2LNT_terms n (substTs ts v s) = substTs (LNN2LNT_terms n ts) v (LNN2LNT_term s)). - intros n; simpl; destruct (eq_nat_dec v n); auto. - simpl in |- *; intros f t0 H; now rewrite H. - reflexivity. - intros n t0 H t1 H0; simpl; 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)