diff --git a/src/abs.ott b/src/abs.ott
index 0e453d6..88a3054 100644
--- a/src/abs.ott
+++ b/src/abs.ott
@@ -109,7 +109,7 @@ formula :: formula_ ::=
   | G ( fn ) = sig :: M :: G_fn_eq_sig
     {{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }}
   | fresh ( x1 , ... , xn , e ) :: M :: fresh
-    {{ coq (my_fresh [[x1 ... xn]] [[e]]) }}
+    {{ coq (fresh_vars [[x1 ... xn]] [[e]]) }}
 
 embed
 {{ coq
@@ -123,7 +123,7 @@ Fixpoint get_val (k:x) (l:list(x*x)): option x :=
       end
   end.
 
-Fixpoint my_subst (e5:e) (l:list (x*x)) : e :=
+Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
   match e5 with
   | e_t t => e_t t
   | e_var x =>
@@ -132,10 +132,10 @@ Fixpoint my_subst (e5:e) (l:list (x*x)) : e :=
               | Some y => e_var y
               end
   | e_fn_call fn e_list =>
-      e_fn_call fn (map (fun e => my_subst e l) e_list)
+      e_fn_call fn (map (fun e => e_var_subst e l) e_list)
   end.
 
-(* we actually need to do some work to convince Coq my_fresh is well founded *)
+(* we actually need to do some work to convince Coq fresh_vars is well founded *)
 Fixpoint e_size (e0 : e) : nat :=
   match e0 with
   | e_t _ => 1
@@ -154,8 +154,8 @@ Program Fixpoint fresh_vars (l : list x) (e0 : e) {measure (e_size e0)} : Prop :
   | e_fn_call fn es =>
       match es with
       | nil => True
-      | e1::es' => my_fresh l e1
-                 /\ my_fresh l (e_fn_call fn es')
+      | e1::es' => fresh_vars l e1
+                 /\ fresh_vars l (e_fn_call fn es')
       end
   end.
 Next Obligation. cbn;lia. Qed.
diff --git a/theories/abs_defs.v b/theories/abs_defs.v
index 644e40b..498bbc3 100644
--- a/theories/abs_defs.v
+++ b/theories/abs_defs.v
@@ -110,7 +110,7 @@ Fixpoint get_val (k:x) (l:list(x*x)): option x :=
       end
   end.
 
-Fixpoint my_subst (e5:e) (l:list (x*x)) : e :=
+Fixpoint e_var_subst (e5:e) (l:list (x*x)) : e :=
   match e5 with
   | e_t t => e_t t
   | e_var x =>
@@ -119,10 +119,10 @@ Fixpoint my_subst (e5:e) (l:list (x*x)) : e :=
               | Some y => e_var y
               end
   | e_fn_call fn e_list =>
-      e_fn_call fn (map (fun e => my_subst e l) e_list)
+      e_fn_call fn (map (fun e => e_var_subst e l) e_list)
   end.
 
-(* we actually need to do some work to convince Coq my_fresh is well founded *)
+(* we actually need to do some work to convince Coq fresh_vars is well founded *)
 Fixpoint e_size (e0 : e) : nat :=
   match e0 with
   | e_t _ => 1
@@ -134,22 +134,21 @@ Lemma size_ge_1: forall e0,
      1 <= e_size e0.
 Proof. destruct e0;cbn;lia. Qed.
 
-Program Fixpoint my_fresh (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
+Program Fixpoint fresh_vars (l : list x) (e0 : e) {measure (e_size e0)} : Prop :=
   match e0 with
   | e_t _ => True
   | e_var x => ~ In x l
   | e_fn_call fn es =>
       match es with
       | nil => True
-      | e1::es' => my_fresh l e1
-                 /\ my_fresh l (e_fn_call fn es')
+      | e1::es' => fresh_vars l e1
+                 /\ fresh_vars l (e_fn_call fn es')
       end
   end.
-
-Next Obligation. cbn;lia. Defined.
+Next Obligation. cbn;lia. Qed.
 Next Obligation.
   induction es';cbn; specialize (size_ge_1 e1);intro; lia.
-Defined.
+Qed.
 
 
 (** definitions *)
@@ -186,7 +185,7 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop :=    (* defn e *)
      red_e F_list s5 e_5 s' e' ->
      red_e F_list s5 (e_fn_call fn5 ((app e_list (app (cons e_5 nil) (app e'_list nil))))) s' (e_fn_call fn5 ((app e_list (app (cons e' nil) (app e'_list nil)))))
  | red_fun_ground : forall (T_x_t_y_list:list (T*x*t*x)) (F'_list F_list:list F) (T_5:T) (fn5:fn) (e5:e) (s5:s),
-      (my_fresh  (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list)   e5 )  ->
-     red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list))  (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5)  s5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) )   (my_subst  e5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) .
+      (fresh_vars  (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => y_ end ) T_x_t_y_list)   e5 )  ->
+     red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list))  (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5)  s5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) )   (e_var_subst  e5   (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (x_,y_) end ) T_x_t_y_list) ) .