diff --git a/hlam.ml b/hlam.ml
index 9c61950..e04f803 100644
--- a/hlam.ml
+++ b/hlam.ml
@@ -8,8 +8,8 @@ type hlam = (* hollow lam *)
   | HVar of id
   | HExf of hlam * Types.ty
   | HPair of hlam * hlam
-  | HLeft of hlam * Types.ty
-  | HRight of hlam * Types.ty
+  | HLeft of hlam * Types.ty (* l (M : t) *)
+  | HRight of hlam * Types.ty (* r (M : t) *)
   | Ref of hlam ref
   | Hole
 
diff --git a/main.ml b/main.ml
index a420b3a..0421af8 100644
--- a/main.ml
+++ b/main.ml
@@ -81,6 +81,7 @@ let check_via_coq (e : lam) (t : ty) : unit =
     then ""
     else "intro. " ^ repeat_intro (n-1)
   in
+  (* build checker.v *)
   let m = fill_ty_map StringMap.empty t in
   let (ty_vars, intro_n) = intro_of_ty m in
   let goal_ty = string_of_ty t in
@@ -120,40 +121,45 @@ let rec interactive (get_instr : unit -> instr) (sl : (interactive_state) list)
 
     try
       match get_instr () with
-      Cmd c -> begin match c with
-          Goal ty ->
-            let rh = Ref (ref Hole) in
-            [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
-          | Undo -> interactive get_instr sq
-          | Qed -> begin match cg with
-            None ->
-              print_error "No current goal" "";
+      Cmd c ->
+        begin match c with
+        Goal ty ->
+          let rh = Ref (ref Hole) in
+          [Some (rh, ty), (Some (rh, ty, []), [])] |> interactive get_instr
+        | Undo -> interactive get_instr sq
+        | Qed -> begin match cg with
+          None ->
+            print_error "No current goal" "";
+            (cg, (g, gs))::sq |> interactive get_instr
+          | Some (h, t) ->
+            let l = lam_of_hlam h
+            |> beta_reduce in
+            (* uncaught Could_not_infer but won't happened
+               because exact only allow typable terms *)
+            if Typing.typecheck [] l t then begin
+              print_string "Ok";
+              (cg, (g, gs))::sq |> interactive get_instr
+            end else begin
+              print_error "Typing failed" "";
+              print_expr l;
+              print_newline ();
+              print_ty t;
               (cg, (g, gs))::sq |> interactive get_instr
-            | Some (h, t) ->
-              let l = lam_of_hlam h
-              |> beta_reduce in
-              if Typing.typecheck [] l t then begin
-                print_string "Ok";
-                (cg, (g, gs))::sq |> interactive get_instr
-              end else begin
-                print_error "Typing failed" "";
-                print_expr l;
-                print_newline ();
-                print_ty t;
-                (cg, (g, gs))::sq |> interactive get_instr
-              end
             end
-          | Check -> begin match cg with
-            None ->
-              print_error "No current goal" "";
-              (cg, (g, gs))::sq |> interactive get_instr
-            | Some (h, t) ->
-              begin try
-                let l = lam_of_hlam h in
-                check_via_coq l t
-              with _ -> print_error "Proof is not over" "";
-              end;
-              (cg, (g, gs))::sq |> interactive get_instr;
+          end
+        | Check -> begin match cg with
+          (* !! Doesn't work with terms containing exfalso
+                and Left / Right !! *)
+          None ->
+            print_error "No current goal" "";
+            (cg, (g, gs))::sq |> interactive get_instr
+          | Some (h, t) ->
+            begin try
+              let l = lam_of_hlam h in
+              check_via_coq l t
+            with _ -> print_error "Proof is not over" "";
+            end;
+            (cg, (g, gs))::sq |> interactive get_instr;
           end
         end
       | Tact t ->
diff --git a/proof.ml b/proof.ml
index a949fd8..31d2b0e 100644
--- a/proof.ml
+++ b/proof.ml
@@ -1,6 +1,6 @@
 open Hlam
 open Lam
-  open Types
+open Types
 
 type context = (id * id * hlam * Types.ty) list
 type goal = hlam * Types.ty * context
@@ -40,19 +40,16 @@ let clean_proof ((g, gs) : proof) : (hlam ref * hlam ref) list ref * proof =
     | None -> None
   in assoc, (g', List.map (clean_goal assoc) gs)
 
-let goal_is_over ((g, _) : proof) : bool =
-  match g with
-  None -> true
-  | Some _ -> false
-
+(* typecheck e t cs types e against t in the typing environment defined
+   by cs *)
 let typecheck (e : lam) (expected_t : Types.ty) (cs : context) : bool =
   let gam_of_ctx : context -> Types.gam =
-    let f = fun (_, var_id, _, ty) -> (var_id, ty) in
-    List.map f
+    (fun (_, var_id, _, ty) -> (var_id, ty)) |>
+    List.map
   in
   let g = gam_of_ctx cs in
   try Typing.typecheck g e expected_t
-  with _ -> raise (TacticFailed "unable to type")
+  with Typing.Could_not_infer -> raise (TacticFailed "couldn't not infer all variable types")
 
 let rec get_term_by_id (hyp : id) : context -> hlam option =
   function
@@ -71,77 +68,78 @@ let next_goal (gs : goal list) : (goal option * goal list) =
   [] -> None, []
   | g :: gs -> Some g, gs
 
-let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
-  match g with
+let get_goal : goal option -> hlam * ty * context =
+  function
   None -> raise (TacticFailed "no current goal")
-  | Some (h, expected_t, cs) ->
-    if typecheck e expected_t cs
+  | Some g -> g
+
+let tact_exact_term ((g, gs) : proof) (e : lam) : proof =
+  let (h, expected_t, cs) = get_goal g in
+  if typecheck e expected_t cs
+  then
+    begin
+    fill h (hlam_of_lam e);
+    next_goal gs
+    end
+  else raise (TacticFailed "type mismatch")
+
+let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
+  let (h, expected_t, cs) = get_goal g in
+  match get_term_by_id hyp cs with
+  Some h' ->
+    if typecheck (lam_of_hlam h') expected_t cs
     then
       begin
-      fill h (hlam_of_lam e);
+      fill h h';
       next_goal gs
       end
     else raise (TacticFailed "type mismatch")
-
-let tact_exact_proof ((g, gs) : proof) (hyp : id) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, expected_t, cs) ->
-    match get_term_by_id hyp cs with
-    Some h' ->
-      if typecheck (lam_of_hlam h') expected_t cs
-      then
-        begin
-        fill h h';
-        next_goal gs
-        end
-      else raise (TacticFailed "type mismatch")
-    | None -> raise (TacticFailed "")
+  | None -> raise (TacticFailed "")
 
 let tact_assumption ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    match get_term_by_type goal_ty cs with
-    None -> (* failwith "assumption failed" *) (g, gs)
-    | Some h' ->
-      fill h h';
-      next_goal gs
+  let (h, goal_ty, cs) = get_goal g in
+  match get_term_by_type goal_ty cs with
+  None -> raise (TacticFailed "no such hypothesis")
+  | Some h' ->
+    fill h h';
+    next_goal gs
 
 let tact_intro ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    match goal_ty with
-    Arr (t1, t2) ->
-      let (hyp_id, var_id) = get_fresh_hyp () in
-      let cs = (hyp_id, var_id, HVar var_id, t1) :: cs in
-      let new_h = Ref (ref Hole) in
-      fill h (HFun ((var_id, t1), new_h));
-      Some (new_h, t2, cs), gs
-    | _ -> (* failwith "expected function" *) (* (g, gs) *)
-            raise (TacticFailed "expected function")
+  let (h, goal_ty, cs) = get_goal g in
+  match goal_ty with
+  Arr (t1, t2) ->
+    let (hyp_id, var_id) = get_fresh_hyp () in
+    let cs = (hyp_id, var_id, HVar var_id, t1) :: cs in
+    let new_h = Ref (ref Hole) in
+    fill h (HFun ((var_id, t1), new_h));
+    Some (new_h, t2, cs), gs
+  | _ -> raise (TacticFailed "expected an implication")
 
 let tact_cut ((g, gs) : proof) (new_t : Types.ty) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    (* subgoal 2 : new_t -> goal_ty *)
-    let arrow_h = Ref (ref Hole) in
-    let arrow_goal = (arrow_h, Arr (new_t, goal_ty), cs) in
-    let gs = arrow_goal :: gs in
-    (* subgoal 1 (main goal) : new_t *)
-    let new_h = Ref (ref Hole) in
-    fill h (HApp (arrow_h, new_h));
-    Some (new_h, new_t, cs), gs
+  let (h, goal_ty, cs) = get_goal g in
+  (* subgoal 2 : new_t -> goal_ty *)
+  let arrow_h = Ref (ref Hole) in
+  let arrow_goal = (arrow_h, Arr (new_t, goal_ty), cs) in
+  let gs = arrow_goal :: gs in
+  (* subgoal 1 (main goal) : new_t *)
+  let new_h = Ref (ref Hole) in
+  fill h (HApp (arrow_h, new_h));
+  Some (new_h, new_t, cs), gs
 
 let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
+  (* check if hypothesis suits apply *)
   let rec is_implied (goal_ty : ty) (t : ty) : bool =
     match t with
     t when t = goal_ty -> true
     | Arr (_, t2) -> is_implied goal_ty t2
     | _ -> false
   in
+  (* supposes is_implied goal_ty impl_ty
+   goal_ty : conclusion of the implication
+   impl_ty : type of the implication
+   impl_h : building the term we will apply to goal_h
+   goal_h : hole of the current goal
+   h : current hole of impl_h*)
   let rec generate_goals (goal_ty : ty) (impl_ty : ty) (impl_h : hlam)
   (goal_h : hlam) (h : hlam) (cs : context) (gs : goal list) : proof =
     match impl_ty with
@@ -151,12 +149,15 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
       let _ = fill goal_h impl_h in
       Some (sub_h, t1, cs), gs
     | Arr (t1, t2) ->
-      let sub_h = Ref (ref Hole) in
-      let new_h = Ref (ref Hole) in
+      (* transforms impl_h from ((f ?x_0) ?) to (((f ?x_0) ?x_1) ?)
+      where ? is h and ?x_i are holes associated with
+      the proof of x_i*)
+      let sub_h = Ref (ref Hole) in (* proof of t1 *)
+      let new_h = Ref (ref Hole) in (* proof of t2 *)
       let _ = fill h sub_h in
       let impl_h = HApp (impl_h, new_h) in
-      let gs = (sub_h, t1, cs) :: gs in
-      generate_goals goal_ty t2 impl_h goal_h new_h cs gs
+      let gs = (sub_h, t1, cs) :: gs in (* add the proof of t1 to goals *)
+      generate_goals goal_ty t2 impl_h goal_h new_h cs gs (* generate_goals for the proof of t2 *)
     | _ -> failwith "impossible"
   in
   let rec get_hyp : context -> (hlam * ty) = function
@@ -164,15 +165,13 @@ let tact_apply ((g, gs) : proof) (hyp_id : id) : proof =
     | (hyp_id', _, h', t') :: _ when hyp_id = hyp_id' -> (h', t')
     | _ :: cs -> get_hyp cs
   in
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (goal_h, goal_ty, cs) ->
-    let impl_h, impl_ty = get_hyp cs in
-    let new_h = Ref (ref Hole) in
-    let impl_h_2 = HApp (impl_h, new_h) in
-    if is_implied goal_ty impl_ty
-    then generate_goals goal_ty impl_ty impl_h_2 goal_h new_h cs gs
-    else raise (TacticFailed "not an implication")
+  let (goal_h, goal_ty, cs) = get_goal g in
+  let impl_h, impl_ty = get_hyp cs in
+  let new_h = Ref (ref Hole) in
+  let impl_h_2 = HApp (impl_h, new_h) in
+  if is_implied goal_ty impl_ty
+  then generate_goals goal_ty impl_ty impl_h_2 goal_h new_h cs gs
+  else raise (TacticFailed "not an implication")
 
 let tact_intros : proof -> proof =
   let rec push (p : proof) =
@@ -183,39 +182,33 @@ let tact_intros : proof -> proof =
   in push
 
 let tact_split ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    match goal_ty with
-    | And(t1, t2) ->
-      let h1 = Ref (ref Hole) in
-      let h2 = Ref (ref Hole) in
-      fill h (HPair (h1, h2));
-      Some (h1, t1, cs), (h2, t2, cs)::gs
-    | _ -> raise (TacticFailed "Not a conjonction")
+  let (h, goal_ty, cs) = get_goal g in
+  match goal_ty with
+  | And(t1, t2) ->
+    let h1 = Ref (ref Hole) in
+    let h2 = Ref (ref Hole) in
+    fill h (HPair (h1, h2));
+    Some (h1, t1, cs), (h2, t2, cs)::gs
+  | _ -> raise (TacticFailed "Not a conjonction")
 
 
 let tact_right ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    match goal_ty with
-    | Or(_, t_r) as t ->
-      let new_h = Ref (ref Hole) in
-      fill h (HRight (new_h, t));
-      Some (new_h, t_r, cs), gs
-    | _ -> raise (TacticFailed "Not a disjunction")
+  let (h, goal_ty, cs) = get_goal g in
+  match goal_ty with
+  | Or(_, t_r) as t ->
+    let new_h = Ref (ref Hole) in
+    fill h (HRight (new_h, t));
+    Some (new_h, t_r, cs), gs
+  | _ -> raise (TacticFailed "Not a disjunction")
 
 let tact_left ((g, gs) : proof) : proof =
-  match g with
-  None -> raise (TacticFailed "no current goal")
-  | Some (h, goal_ty, cs) ->
-    match goal_ty with
-    | Or(t_l, _) as t->
-      let new_h = Ref (ref Hole) in
-      fill h (HLeft (new_h, t));
-      Some (new_h, t_l, cs), gs
-    | _ -> raise (TacticFailed "Not a disjunction")
+  let (h, goal_ty, cs) = get_goal g in
+  match goal_ty with
+  | Or(t_l, _) as t->
+    let new_h = Ref (ref Hole) in
+    fill h (HLeft (new_h, t));
+    Some (new_h, t_l, cs), gs
+  | _ -> raise (TacticFailed "Not a disjunction")
 
 let rec apply_tactic (p : proof) (t : tactic) : proof =
   match t with
@@ -231,7 +224,3 @@ let rec apply_tactic (p : proof) (t : tactic) : proof =
   | TLeft -> tact_left p
   | TTry t -> try apply_tactic p t with TacticFailed _ -> p
 
-
-let tact_try (p : proof) (t : tactic) : proof =
-  try apply_tactic p t
-  with TacticFailed _ -> p
diff --git a/tests/alpha_equiv/free_var_1.lam b/tests/alpha_equiv/free_var_1.lam
new file mode 100644
index 0000000..1661b7d
--- /dev/null
+++ b/tests/alpha_equiv/free_var_1.lam
@@ -0,0 +1 @@
+x & x
diff --git a/tests/alpha_equiv/free_var_2.lam b/tests/alpha_equiv/free_var_2.lam
new file mode 100644
index 0000000..9d87069
--- /dev/null
+++ b/tests/alpha_equiv/free_var_2.lam
@@ -0,0 +1 @@
+x & y
diff --git a/tests/alpha_equiv/free_var_3.lam b/tests/alpha_equiv/free_var_3.lam
new file mode 100644
index 0000000..9c23611
--- /dev/null
+++ b/tests/alpha_equiv/free_var_3.lam
@@ -0,0 +1 @@
+x (fun (y : A) => y) & x (fun (z : A) => z)
diff --git a/tests/alpha_equiv/not_same_but_same_order.lam b/tests/alpha_equiv/not_same_but_same_order.lam
new file mode 100644
index 0000000..2ac7fbc
--- /dev/null
+++ b/tests/alpha_equiv/not_same_but_same_order.lam
@@ -0,0 +1 @@
+(fun (x : A) => fun (y : B) => x y) & (fun (x : A) => fun (y : B) => y x)
diff --git a/tests/alpha_equiv/not_same_free.lam b/tests/alpha_equiv/not_same_free.lam
new file mode 100644
index 0000000..d8f1cce
--- /dev/null
+++ b/tests/alpha_equiv/not_same_free.lam
@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (z : A) => z)
diff --git a/tests/alpha_equiv/same_but_different_order.lam b/tests/alpha_equiv/same_but_different_order.lam
new file mode 100644
index 0000000..896a9a3
--- /dev/null
+++ b/tests/alpha_equiv/same_but_different_order.lam
@@ -0,0 +1 @@
+(fun (x : A) => fun (y : B) => x y) & (fun (y : A) => fun (x : B) => y x) 
diff --git a/tests/alpha_equiv/same_free.lam b/tests/alpha_equiv/same_free.lam
new file mode 100644
index 0000000..bdbec14
--- /dev/null
+++ b/tests/alpha_equiv/same_free.lam
@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (y : A) => z)
diff --git a/tests/alpha_equiv/same_term_but_not_same_type.lam b/tests/alpha_equiv/same_term_but_not_same_type.lam
new file mode 100644
index 0000000..5f85d9f
--- /dev/null
+++ b/tests/alpha_equiv/same_term_but_not_same_type.lam
@@ -0,0 +1 @@
+(fun (x : A) => z) & (fun (y : B) => z)
diff --git a/tests/free_or_not.lam b/tests/free_or_not.lam
new file mode 100644
index 0000000..e603a9f
--- /dev/null
+++ b/tests/free_or_not.lam
@@ -0,0 +1 @@
+(fun (z : A) => (fun (x : A) => z)) (fun (y : A) => z)