proposition: Lemma subSubAllTerm (t : fol.Term L) (m : nat -> fol.Term L) (v : nat) (s : fol.Term L): substT (subAllTerm t m) v s = subAllTerm t (fun n : nat => substT (m n) v s).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => substTs (subAllTerms n ts m) v s = subAllTerms n ts (fun n : nat => substT (m n) v s)). - intro n; simpl; auto. - intros f t0 H; simpl; rewrite H; auto. - auto. - intros n t0 H t1 H0; simpl; now rewrite H, H0. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)