proposition: Lemma freeVarInterpTerm (v1 v2 : nat -> U M) (t : Term L): (forall x : nat, List.In x (freeVarT t) -> v1 x = v2 x) -> interpTerm v1 t = interpTerm v2 t.
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : Terms L n) => forall f : naryFunc (U M) n, (forall x : nat, List.In x (freeVarTs ts) -> v1 x = v2 x) -> interpTerms n f v1 ts = interpTerms n f v2 ts); simpl. - intros n H; apply H; left; auto. - intros f t0 H H0; apply H. intros x H1; apply H0, H1. - reflexivity. - intros n t0 H t1 H0 f H1. rewrite H. apply H0. intros x H2; apply H1. + unfold freeVarTs; apply in_or_app. right; apply H2. + intros x H2; apply H1. unfold freeVarTs; apply in_or_app; left. apply H2. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)