fact: Definition extract_list (le : list expr) (vars : nat) := if max_arity_list le vars then let (lp, lc) := fold_split le nil nil in let lp' := le ++ lp in match decompose vars nil lp' lc with | Some p => Eprog p lc | None => Eabort end else Eabort.
imports: Coq(ZArith Reals List Psatz) Xreal Tree