proposition: Lemma app_converges (s t : term) : (converges (s t)) -> converges s /\ converges t.
proof: Proof. intros H. split; destruct H as [u [H lu]];inv lu; eapply eproc_equiv in H; eapply eval_seval in H; destruct H as [n H]; inv H; [exists (lam u) | exists (lam v)];(split;[|auto]); eapply eproc_equiv; eapply seval_eval; eassumption. Qed.
imports: Coq.Logic.ConstructiveEpsilon