diff --git a/Coq/f.v b/Coq/f.v
index 1b11d30ff5790a7c3515d6e71d0928f67b643d59..415c537a5fb431ce3f896ce3979af453180d2b8c 100644
--- a/Coq/f.v
+++ b/Coq/f.v
@@ -132,7 +132,7 @@ Inductive logterm : Type :=
  | LAbs : logterm -> logterm
  | LApp : logterm -> logtermlist -> logterm
  | LMetavar : nat -> logterm
- | LMetasubst : logterm -> nat -> logtermlist -> logterm
+ | LMetasubst : logterm -> logtermlist -> logterm
 with logtermlist : Type :=
  | LLVar : nat -> logtermlist
  | LLList : list logterm -> logtermlist.
@@ -156,7 +156,7 @@ Fixpoint logterm_liftt (n : nat) (t : logterm) : logterm :=
   | LAbs t => LAbs (logterm_liftt n t)
   | LApp t p => LApp (logterm_liftt n t) (logtermlist_liftt n p)
   | LMetavar m => if m <? n then LMetavar m else LMetavar (S m)
-  | LMetasubst t m p => LMetasubst (logterm_liftt n t) m (logtermlist_liftt n p)
+  | LMetasubst t p => LMetasubst (logterm_liftt n t) (logtermlist_liftt n p)
  end
 with logtermlist_liftt (n : nat) (p : logtermlist) : logtermlist :=
  match p with
@@ -172,7 +172,7 @@ Fixpoint logterm_liftp (n : nat) (t : logterm) : logterm :=
   | LAbs t => LAbs (logterm_liftp n t)
   | LApp t p => LApp (logterm_liftp n t) (logtermlist_liftp n p)
   | LMetavar m => LMetavar m
-  | LMetasubst t m p => LMetasubst (logterm_liftp n t) m (logtermlist_liftp n p)
+  | LMetasubst t p => LMetasubst (logterm_liftp n t) (logtermlist_liftp n p)
  end
 with logtermlist_liftp (n : nat) (p : logtermlist) : logtermlist :=
  match p with
@@ -193,7 +193,7 @@ Fixpoint logterm_substt (n : nat) (t : logterm) (u : logterm) : logterm :=
     | Eq => u
     | Gt => LMetavar (pred m)
    end
-  | LMetasubst t m p => LMetasubst (logterm_substt n t u) m (logtermlist_substt n p u)
+  | LMetasubst t p => LMetasubst (logterm_substt n t u) (logtermlist_substt n p u)
  end
 with logtermlist_substt (n : nat) (p : logtermlist) (u : logterm) : logtermlist :=
  match p with
@@ -209,7 +209,7 @@ Fixpoint logterm_substp (n : nat) (t : logterm) (p : logtermlist) : logterm :=
   | LAbs t => LAbs (logterm_substp n t p)
   | LApp t q => LApp (logterm_substp n t p) (logtermlist_substp n q p)
   | LMetavar m => LMetavar m
-  | LMetasubst t m q => LMetasubst (logterm_substp n t p) m (logtermlist_substp n q p)
+  | LMetasubst t q => LMetasubst (logterm_substp n t p) (logtermlist_substp n q p)
  end
 with logtermlist_substp (n : nat) (q : logtermlist) (p : logtermlist) : logtermlist :=
  match q with
@@ -233,10 +233,10 @@ Fixpoint logterm_to_term (t : logterm) : term :=
     | LLList p => fold_right (fun u t => App t u) (logterm_to_term t) (map logterm_to_term p)
    end
   | LMetavar m => Var 0
-  | LMetasubst t m p =>
+  | LMetasubst t p =>
    match p with
     | LLVar m => Var 0
-    | LLList p => term_subst m (logterm_to_term t) (map logterm_to_term p)
+    | LLList p => term_subst 0 (logterm_to_term t) (map logterm_to_term p)
    end
  end.
 
@@ -345,7 +345,7 @@ Definition redcand : form :=
   )
   (FForallt (FForallt (FForallp
    (FImp
-    (FIn (LApp (LMetasubst (LMetavar 1) 0 (LLList [LMetavar 0])) (LLVar 0)) 0)
+    (FIn (LApp (LMetasubst (LMetavar 1) (LLList [LMetavar 0])) (LLVar 0)) 0)
     (FIn (LApp (LApp (LAbs (LMetavar 1)) (LLList [LMetavar 0])) (LLVar 0)) 0)
    )
   ))).