proposition: Theorem extract_correct : forall e vars, match extract e (length vars) with | Eabort => True | Eprog lp lc => eval_real' lp vars lc = eval e vars end.
proof: Proof. intros e vars. change (eval e vars) with (eval (nth O (e :: nil) (Econst (Int 0))) vars). unfold eval_real', extract. generalize (extract_list_correct (e :: nil) vars). destruct extract_list; [easy | ]. intros H. now specialize (H O (Nat.lt_0_succ _)). Qed.
imports: Coq(ZArith Reals List Psatz) Xreal Tree