proposition: Lemma computesExpStart t1 (tt1 : TT t1) (f : t1) (fExt : term): proc fExt -> {v :term & computesExp tt1 f fExt v} -> computes tt1 f fExt.
proof: Proof. intros ? (?&?&?). replace fExt with x. tauto. apply unique_normal_forms. eapply e. eapply H. destruct e as [e ?]. now rewrite e. Qed.
imports: String