diff --git a/src/Infer.ml b/src/Infer.ml
index 8a0ef2a..358152b 100644
--- a/src/Infer.ml
+++ b/src/Infer.ml
@@ -54,7 +54,30 @@ module Make(T : Utils.Functor) = struct
   let rec bind (ty : STLC.ty) (k : Constraint.variable -> ('a, 'e) t) : ('a, 'e) t =
     (* Feel free to postpone implementing this function
        until you implement the Annot case below. *)
-    Utils.not_yet "Infer.bind" (ty, k, fun () -> bind)
+    match ty with
+    | Constr Var x -> k x
+    | Constr Arrow (ta,tb) ->
+        let w,ap,bp = Var.fresh "w",Var.fresh "a",Var.fresh "b" in
+        Exist(ap,None,
+        Exist(bp,None,
+        Map(
+          Conj(
+            bind ta (fun x -> eq x ap),
+            Conj(
+              bind tb (fun x -> eq x bp),
+              Exist(w,Some (Structure.Arrow (ap,bp)),k w)
+            )
+          ),
+          fun ((),((),t)) -> t
+        )))
+    | Constr Prod l -> 
+        let w = Var.fresh "w" in
+        let arr = List.map (fun ty -> (ty,Var.fresh "t")) l in
+        List.fold_right (fun (_,ap) con -> Exist(ap,None,con)) arr (
+          List.fold_right (fun (tt,av) con -> Map(Conj(bind tt (fun x -> eq x av),con),fun ((),t) -> t)) arr (
+            Exist(w,Some (Structure.Prod (List.map snd arr)),k w)
+          ))
+    end
 
   (** This function generates a typing constraint from an untyped term:
       [has_type env t w] generates a constraint [C] which contains [w] as
@@ -99,24 +122,29 @@ module Make(T : Utils.Functor) = struct
         let tau,a,b = Var.fresh "τ",Var.fresh "α", Var.fresh "β" in
         let newenv = Env.add x a env in
         Exist(tau, Some (Arrow(a, b)),
-          Map(Conj(
-            has_type newenv t b,
-            eq tau w
-          ), fun t -> let (x,_) = p in x) (* term * unit -> term isomorphism *)
+          Map(
+            Conj(
+              Conj(
+                has_type newenv t b,
+                eq tau w 
+              ),
+              decode tau
+            ),
+            fun ((tt,()),ty) -> Abs(x, ty, tt))
         )
     | Untyped.Let (x, t, u) ->
       Utils.not_yet "Infer.has_type: Let case" (env, x, t, u, fun () -> has_type)
     | Untyped.Annot (t, ty) ->
-      Utils.not_yet "Infer.has_type: Let case" (env, t, ty, bind, fun () -> has_type)
+        bind (fun w -> has_type env w) ty
     | Untyped.Tuple ts ->
       let (t1, t2) = assume_pair ts in
-      Utils.not_yet "Infer.has_type: Let case" (env, t1, t2, fun () -> has_type)
+      Utils.not_yet "Infer.has_type: Tuple case" (env, t1, t2, fun () -> has_type)
     | Untyped.LetTuple (xs, t, u) ->
       let (x1, x2) = assume_pair xs in
-      Utils.not_yet "Infer.has_type: Let case" (env, x1, x2, t, u, fun () -> has_type)
+      Utils.not_yet "Infer.has_type: LetTuple case" (env, x1, x2, t, u, fun () -> has_type)
     | Do p ->
       (* Feel free to postone this until you start looking
          at random generation. Getting type inference to
          work on all the other cases is a good first step. *)
-      Utils.not_yet "Infer.has_type: Let case" (env, p, fun () -> has_type)
+      Utils.not_yet "Infer.has_type: Do case" (env, p, fun () -> has_type)
 end