proposition: Lemma computesExpStep t1 t2 (tt1 : TT t1) (tt2 : TT t2) (f : t1 -> t2) (s:term) (fExt : term): eval s fExt -> closed s -> (forall (y : t1) (yExt : term), computes tt1 y yExt -> {v : term & computesExp tt2 (f y) (app s yExt) v}%type) -> computesExp (tt1 ~> tt2) f s fExt.
proof: Proof. intros ? ? H. split. assumption. split. split. now rewrite <-H0. now destruct H0. intros ? ? exted. edestruct H as (v&?&?). eassumption. eexists v. split. rewrite H0 in e. now rewrite e. eauto. Qed.
imports: String