proposition: Lemma subAllTerm_ext (t : fol.Term L) : forall (m1 m2 : nat -> fol.Term L), (forall m : nat, In m (freeVarT t) -> m1 m = m2 m) -> subAllTerm t m1 = subAllTerm t 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, (forall m : nat, In m (freeVarTs ts) -> m1 m = m2 m) -> subAllTerms n ts m1 = subAllTerms n ts m2); simpl. - intros n m1 m2 H; apply H; auto. - intros f t0 H m1 m2 H0; rewrite (H m1 m2). + reflexivity. + intros m H1; apply H0; apply H1. - reflexivity. - intros n t0 H t1 H0 m1 m2 H1; rewrite (H m1 m2). + rewrite (H0 m1 m2). * reflexivity. * intros m H2; apply H1. unfold freeVarTs; fold (freeVarTs t1). apply in_or_app; auto. + intros m H2; apply H1. unfold freeVarTs; fold (freeVarTs t1); apply in_or_app; auto. Qed.
imports: Coq(Ensembles List Arith Peano_dec) hydras.Ackermann(ListExt folProof folLogic folLogic2 folProp) hydras(folReplace subProp Compat815) Coq(Lia)