proposition: Lemma extApp t1 t2 {tt1:TT t1} {tt2 : TT t2} (f: t1 -> t2) (x:t1) (Hf : computable f) (Hx : computable x) : app (ext f) (ext x) >* ext (f x).
proof: Proof. unfold ext, extApp'. destruct Hf, Hx. destruct extCorrect0 as (? & correct0). destruct correct0 as (?&?&?). tauto. Qed.
imports: String