proposition: Lemma computesTyArr t1 t2 (tt1 : TT t1) (tt2 : TT t2) f fExt : proc fExt -> (forall (y : t1) (yExt : term), computes tt1 y yExt -> {v : term & eval (app fExt yExt) v * (proc v -> computes tt2 (f y) v)}%type) -> computes (tt1 ~> tt2) f fExt.
proof: Proof. intros ? H'. split;[assumption|]. intros y yExt yCorrect. edestruct H' as (?&(R&?) & H''). eassumption. eexists. split. eassumption. eapply H''. split. 2:assumption. rewrite <- R. apply app_closed. now destruct H. specialize (computesProc yCorrect) as []. easy. Qed.
imports: String