fact: Fixpoint insertCast t1 (tt1 : TT t1) Y (R: encodable Y) {struct tt1}: forall (cast : projT1 (resType tt1) -> Y) (f : t1), projT1 (changeResType tt1 (TyB Y)) := match tt1 with TyB _ _ => fun cast x => cast x | TyArr _ _ tt11 tt12 => fun cast f x=> (insertCast (tt1:=tt12) R cast (f x)) end.
imports: String