proposition: Lemma subAllSubAllTerm (t : fol.Term L) : forall (m1 m2 : nat -> fol.Term L), subAllTerm (subAllTerm t m1) m2 = subAllTerm t (fun n : nat => subAllTerm (m1 n) m2).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : fol.Terms L n) => forall m1 m2 : nat -> fol.Term L, subAllTerms n (subAllTerms n ts m1) m2 = subAllTerms n ts (fun n : nat => subAllTerm (m1 n) m2)); simpl. - reflexivity. - intros f t0 H m1 m2; now rewrite H. - reflexivity. - intros n t0 H t1 H0 m1 m2; 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)