proposition: Lemma subInterpRel (value : nat -> U M) (n : nat) (ts : Terms L n) (v : nat) (s : Term L) (r : naryRel (U M) n): interpRels n r (updateValue value v (interpTerm value s)) ts <-> interpRels n r value (substTs ts v s).
proof: Proof. induction ts as [| n t ts Hrects]. - simpl; tauto. - simpl; rewrite <- subInterpTerm; apply Hrects. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)