proposition: Lemma freeVarInterpRel (v1 v2 : nat -> U M) (n : nat) (ts : Terms L n) (r : naryRel (U M) n): (forall x : nat, List.In x (freeVarTs ts) -> v1 x = v2 x) -> interpRels n r v1 ts -> interpRels n r v2 ts.
proof: Proof. intros H; induction ts as [| n t ts Hrects]; simpl in |- *. - auto. - rewrite (freeVarInterpTerm v1 v2). + apply Hrects. intros x H0; apply H. unfold freeVarTs; apply in_or_app; right; apply H0. + intros x H0; apply H. unfold freeVarTs; apply in_or_app; left; apply H0. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)