match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]