proposition: Lemma Eval_converges s : converges s <-> converges (Eval (ext s)).
proof: Proof. Proof with eauto. split; intros H. - destruct (eval_converges H) as [t Ht]. pose proof (eval_Eval Ht) as He. rewrite He. eexists;split;[reflexivity|Lproc]. - destruct H as [x [H l]]. apply Eval_eval in H;try Lproc. destruct H as [t' [? t]]. exists t'. destruct t. split. now rewrite H0. auto. Qed.