inferType d g (ELetRGN tr1 ta v) =
  case (inferType d g . valToExp) v of 
    Nothing -> Nothing
    Just tv -> 
      if (S.member tr1 d) && (S.member ta d) && isJust tv
        then let FForall gr2 (FArrow (FArrow (FArrow (RGN tr1 (FVar gr2)) (RGN (FVar gr2) (gr2))) (RGNHandle (FVar gr2))) (RGN (FVar gr2) ta)) = tv
              in if gr2 == gr2' && gr2' == gr2'' && gr2'' == gr2''' && gr2''' == gr2'''' && gr2'''' == gr2'''''
                   then Just $ RGN tr1 ta
                   else Nothing
        else Nothing