+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end
+ | WCoerVar _ => None
+ end else None
+ | _ => None
+end.
+
+Definition isCSP (ce:@CoreExpr CoreVar) : ??(WeakExprVar * WeakTypeVar * CoreType) :=
+match ce with
+ | (CoreEApp (CoreEApp (CoreEVar v) (CoreEType (TyVarTy ec))) (CoreEType tbody))
+ => if coreName_eq hetmet_csp_name (coreVarCoreName v) then
+ match coreVarToWeakVar ec with
+ | WExprVar _ => None
+ | WTypeVar tv => match coreVarToWeakVar v with
+ | WExprVar v' => Some (v',tv,tbody)
+ | _ => None
+ end