diff --git a/lam.ml b/lam.ml
index 12150e5..e74a519 100644
--- a/lam.ml
+++ b/lam.ml
@@ -10,31 +10,28 @@ type lam =
 
 (** alpha renaming in a deterministic way *)
 let alpha_convert (e : lam) : lam =
-  let cpt_ty = ref 0 in (* id cpt for type variables *)
   let cpt_var = ref 0 in (* id cpt for variables *)
   let generator (cpt : int ref) : id = (* id generator *)
-    let v = string_of_int !cpt
+    let v = "__"^(string_of_int !cpt)
     in incr cpt; v
 
   in let renamed = ref []
-  in let rename (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *)
+  in let new_ren_var (cpt : int ref) (var : id) : id = (* checks if a variable already has a new id, or generates one *)
+    let var' = generator cpt in (
+      renamed := (var, var')::!renamed;
+      var'
+    )
+
+  in let get_ren_var (var : id) : id = (* returns var if not found *)
     match List.assoc_opt var !renamed with
       | Some var' -> var'
-      | None -> let var' = generator cpt in (
-          renamed := (var, var')::!renamed;
-          var')
-
-  in let rec alpha_ty (t : Types.ty) : Types.ty = match t with
-    Arr (t1, t2) -> Arr (alpha_ty t1, alpha_ty t2)
-    | TVar (v) -> TVar (rename cpt_ty v)
-    | Bot -> Bot
-
+      | None -> var
   
   in let rec alpha_aux (e : lam) : lam = match e with (* actual renaming *)
-    Fun ((v, t), e) -> Fun ((rename cpt_var v, alpha_ty t), alpha_aux e)
+    Fun ((v, t), e) -> Fun ((new_ren_var cpt_var v, t), alpha_aux e)
     | App (e1, e2) -> App (alpha_aux e1, alpha_aux e2)
-    | Var v -> Var (rename cpt_var v)
-    | Exf (e, s) -> Exf (alpha_aux e, s)
+    | Var v -> Var (get_ren_var v)
+    | Exf (e, t) -> Exf (alpha_aux e, t)
   in alpha_aux e