fact: Definition eval_generic_body {A} (ops : operations A) values op := let nth n := nth n values (unknown ops) in match op with | Forward u => nth u | Unary o u => unary ops o (nth u) | Binary o u v => binary ops o (nth u) (nth v) end :: values.
imports: Coq(ZArith Reals List Psatz) Xreal Tree