fact: Definition updateValue (value : nat -> U M) (n : nat) (v : U M) (x : nat) : U M := match eq_nat_dec n x with | left _ => v | right _ => value x end.
imports: Coq(Ensembles List Vector Arith) hydras.Ackermann(ListExt folProof folProp) Coq(Peano_dec) hydras.Ackermann(misc) hydras.Ackermann(NewNotations)