fact: Fixpoint changeResType t1 t2 (tt1:TT t1) (tt2 : TT t2) : {t & TT t}:= match tt1 with TyB _ _ => existT _ t2 tt2 | TyArr _ _ tt11 tt12 => existT _ _ (TyArr tt11 (projT2 (changeResType tt12 tt2))) end.
imports: String