proposition: Lemma subInterpTerm (value : nat -> U M) (t : Term L) (v : nat) (s : Term L): interpTerm (updateValue value v (interpTerm value s)) t = interpTerm value (substT t v s).
proof: Proof. elim t using Term_Terms_ind with (P0 := fun (n : nat) (ts : Terms L n) => forall f : naryFunc (U M) n, interpTerms n f (updateValue value v (interpTerm value s)) ts = interpTerms n f value (substTs ts v s)); simpl. - intro n; unfold updateValue; induction (eq_nat_dec v n); reflexivity. - intros f t0 H; rewrite H. + reflexivity. - reflexivity. - intros n t0 H t1 H0 f; rewrite H; apply H0. Qed.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)