proposition: Lemma subInterpFormula1 (value : nat -> U M) (f : Formula L) (v : nat) (s : Term L): interpFormula (updateValue value v (interpTerm value s)) f -> interpFormula value (substF f v s).
proof: Proof. induction (subInterpFormula value f v s); auto. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)