diff --git a/Coq/f.v b/Coq/f.v
new file mode 100644
index 0000000000000000000000000000000000000000..e56ab83a016f1f9b66415f3ac41d7c48438c32cb
--- /dev/null
+++ b/Coq/f.v
@@ -0,0 +1,909 @@
+Require Import Program.Wf.
+Require Import JMeq.
+Require Import Arith.
+Require Import List.
+Import ListNotations.
+Import EqNotations.
+Inductive type : Type :=
+ | TVar : nat -> type
+ | TArrow : type -> type -> type
+ | TForall : type -> type.
+Fixpoint type_lift (n : nat) (T : type) : type :=
+ match T with
+  | TVar m => if m <? n then TVar m else TVar (S m)
+  | TArrow T U => TArrow (type_lift n T) (type_lift n U)
+  | TForall T => TForall (type_lift (S n) T)
+ end.
+Fixpoint type_subst (n : nat) (T : type) (U : type) : type :=
+ match T with
+  | TVar m =>
+   match m ?= n with
+    | Lt => TVar m
+    | Eq => U
+    | Gt => TVar (pred m)
+   end
+  | TArrow T1 T2 => TArrow (type_subst n T1 U) (type_subst n T2 U)
+  | TForall T => TForall (type_subst (S n) T (type_lift 0 U))
+ end.
+
+Inductive fterm : Type :=
+ | FVar : nat -> fterm
+ | FAbs : type -> fterm -> fterm
+ | FApp : fterm -> fterm -> fterm
+ | FTAbs : fterm -> fterm
+ | FTApp : fterm -> type -> fterm.
+Definition term1 : fterm :=  FTAbs (FAbs (TVar 0) (FVar 0)).
+Definition term2 : fterm :=  FAbs (TForall (TArrow (TVar 0) (TVar 0))) (FApp (FTApp (FVar 0) (TForall (TArrow (TVar 0) (TVar 0)))) (FVar 0)).
+Fixpoint type_get (context : list type) (t : fterm) : type :=
+ match t with
+  | FVar n => nth n context (TVar 0)
+  | FAbs T t => TArrow T (type_get (T::context) t)
+  | FApp t u =>
+   match type_get context t with
+    | TArrow T U => U
+    | _ => TVar 0
+   end
+  | FTAbs t => TForall (type_get (map (type_lift 0) context) t)
+  | FTApp t T =>
+   match type_get context t with
+    | TForall U => type_subst 0 U T
+    | _ => TVar 0
+   end
+ end.
+Fixpoint type_correct (context : list type) (t : fterm) : Prop :=
+ match t with
+  | FVar n => n < length context
+  | FAbs T t => type_correct (T::context) t
+  | FApp t u => type_correct context t /\ type_correct context u /\ exists T, type_get context t = TArrow (type_get context u) T
+  | FTAbs t => type_correct (map (type_lift 0) context) t
+  | FTApp t T => type_correct context t /\ exists T, type_get context t = TForall T
+ end.
+
+Inductive term : Type :=
+ | Var : nat -> term
+ | Abs : term -> term
+ | App : term -> term -> term.
+Fixpoint fterm_to_term (t : fterm) : term :=
+ match t with
+  | FVar n => Var n
+  | FAbs T t => Abs (fterm_to_term t)
+  | FApp t u => App (fterm_to_term t) (fterm_to_term u)
+  | FTAbs t => fterm_to_term t
+  | FTApp t T => fterm_to_term t
+ end.
+Fixpoint term_equal (t : term) (u : term) : bool :=
+ match t, u with
+  | Var m, Var n => m =? n
+  | Abs t, Abs u => term_equal t u
+  | App t1 t2, App u1 u2 => andb (term_equal t1 u1) (term_equal t2 u2)
+  | _, _ => false
+ end.
+Fixpoint term_lift (n : nat) (t : term) : term :=
+ match t with
+  | Var m => if m <? n then Var m else Var (S m)
+  | Abs t => Abs (term_lift (S n) t)
+  | App t u => App (term_lift n t) (term_lift n u)
+ end.
+Fixpoint term_subst (n : nat) (t : term) (p : list term) : term :=
+ match t with
+  | Var m => if m <? n then Var m else nth (m - n) p (Var (pred m))
+  | Abs t => Abs (term_subst (S n) t (map (term_lift 0) p))
+  | App t u => App (term_subst n t p) (term_subst n u p)
+ end.
+
+Inductive logterm : Type :=
+ | LVar : nat -> logterm
+ | LAbs : logterm -> logterm
+ | LApp : logterm -> logtermlist -> logterm
+ | LMetavar : nat -> logterm
+ | LMetasubst : logterm -> nat -> logtermlist -> logterm
+with logtermlist : Type :=
+ | LLVar : nat -> logtermlist
+ | LLList : list logterm -> logtermlist.
+Fixpoint term_to_logterm (t : term) : logterm :=
+ match t with
+  | Var m => LVar m
+  | Abs t => LAbs (term_to_logterm t)
+  | App t u => LApp (term_to_logterm t) (LLList [term_to_logterm u])
+ end.
+Fixpoint termlist_to_logtermlist (p : list term) : logtermlist :=
+ LLList (map term_to_logterm p).
+Fixpoint logterm_liftt (n : nat) (t : logterm) : logterm :=
+ match t with
+  | LVar m => LVar m
+  | 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)
+ end
+with logtermlist_liftt (n : nat) (p : logtermlist) : logtermlist :=
+ match p with
+  | LLVar m => LLVar m
+  | LLList p => LLList (map (logterm_liftt n) p)
+ end.
+Fixpoint logterm_liftp (n : nat) (t : logterm) : logterm :=
+ match t with
+  | LVar m => LVar m
+  | 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)
+ end
+with logtermlist_liftp (n : nat) (p : logtermlist) : logtermlist :=
+ match p with
+  | LLVar m => if m <? n then LLVar m else LLVar (S m)
+  | LLList p => LLList (map (logterm_liftp n) p)
+ end.
+Fixpoint logterm_substt (n : nat) (t : logterm) (u : logterm) : logterm :=
+ match t with
+  | LVar n => LVar n
+  | LAbs t => LAbs (logterm_substt n t u)
+  | LApp t p => LApp (logterm_substt n t u) (logtermlist_substt n p u)
+  | LMetavar m =>
+   match m ?= n with
+    | Lt => LMetavar m
+    | Eq => u
+    | Gt => LMetavar (pred m)
+   end
+  | LMetasubst t m p => LMetasubst (logterm_substt n t u) m (logtermlist_substt n p u)
+ end
+with logtermlist_substt (n : nat) (p : logtermlist) (u : logterm) : logtermlist :=
+ match p with
+  | LLVar m => LLVar m
+  | LLList p => LLList (map (fun t => logterm_substt n t u) p)
+ end.
+Fixpoint logterm_substp (n : nat) (t : logterm) (p : logtermlist) : logterm :=
+ match t with
+  | LVar n => LVar n
+  | 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)
+ end
+with logtermlist_substp (n : nat) (q : logtermlist) (p : logtermlist) : logtermlist :=
+ match q with
+  | LLVar m =>
+   match m ?= n with
+    | Lt => LLVar m
+    | Eq => p
+    | Gt => LLVar (pred m)
+   end
+  | LLList q => LLList (map (fun t => logterm_substp n t p) q)
+ end.
+Fixpoint logterm_to_term (t : logterm) : term :=
+ match t with
+  | LVar n => Var n
+  | LAbs t => Abs (logterm_to_term t)
+  | LApp t p =>
+   match p with
+    | LLVar m => Var 0
+    | 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 =>
+   match p with
+    | LLVar m => Var 0
+    | LLList p => term_subst m (logterm_to_term t) (map logterm_to_term p)
+   end
+ end.
+
+Inductive form : Type :=
+ | FIn : logterm -> nat -> form
+ | FBool : form
+ | FImp : form -> form -> form
+ | FConj : form -> form -> form
+ | FForallt : form -> form
+ | FForallp : form -> form
+ | FForall2 : form -> form.
+Fixpoint form_substt (n : nat) (f : form) (t : logterm) : form :=
+ match f with
+  | FIn u m => FIn (logterm_substt n u t) m
+  | FBool => FBool
+  | FImp f g => FImp (form_substt n f t) (form_substt n g t)
+  | FConj f g => FConj (form_substt n f t) (form_substt n g t)
+  | FForallt f => FForallt (form_substt (S n) f (logterm_liftt 0 t))
+  | FForallp f => FForallp (form_substt n f t)
+  | FForall2 f => FForall2 (form_substt n f t)
+ end.
+Fixpoint form_substp (n : nat) (f : form) (p : logtermlist) : form :=
+ match f with
+  | FIn t m => FIn (logterm_substp n t p) m
+  | FBool => FBool
+  | FImp f g => FImp (form_substp n f p) (form_substp n g p)
+  | FConj f g => FConj (form_substp n f p) (form_substp n g p)
+  | FForallt f => FForallt (form_substp n f p)
+  | FForallp f => FForallp (form_substp (S n) f (logtermlist_liftp 0 p))
+  | FForall2 f => FForall2 (form_substp n f p)
+ end.
+Fixpoint form_liftt (n : nat) (f : form) : form :=
+ match f with
+  | FIn t m => FIn (logterm_liftt n t) m
+  | FBool => FBool
+  | FImp f g => FImp (form_liftt n f) (form_liftt n g)
+  | FConj f g => FConj (form_liftt n f) (form_liftt n g)
+  | FForallt f => FForallt (form_liftt (S n) f)
+  | FForallp f => FForallp (form_liftt n f)
+  | FForall2 f => FForall2 (form_liftt n f)
+ end.
+Fixpoint form_liftp (n : nat) (f : form) : form :=
+ match f with
+  | FIn t m => FIn (logterm_liftp n t) m
+  | FBool => FBool
+  | FImp f g => FImp (form_liftp n f) (form_liftp n g)
+  | FConj f g => FConj (form_liftp n f) (form_liftp n g)
+  | FForallt f => FForallt (form_liftp n f)
+  | FForallp f => FForallp (form_liftp (S n) f)
+  | FForall2 f => FForall2 (form_liftp n f)
+ end.
+Fixpoint form_lift2 (n : nat) (f : form) : form :=
+ match f with
+  | FIn t m => if m <? n then FIn t m else FIn t (S m)
+  | FBool => FBool
+  | FImp f g => FImp (form_lift2 n f) (form_lift2 n g)
+  | FConj f g => FConj (form_lift2 n f) (form_lift2 n g)
+  | FForallt f => FForallt (form_lift2 n f)
+  | FForallp f => FForallp (form_lift2 n f)
+  | FForall2 f => FForall2 (form_lift2 (S n) f)
+ end.
+Fixpoint form_subst2 (n : nat) (f : form) (g : form) : form :=
+ match f with
+  | FIn t m =>
+   match m ?= n with
+    | Lt => FIn t m
+    | Eq => form_substt 0 g t
+    | Gt => FIn t (pred m)
+   end
+  | FBool => FBool
+  | FImp f1 f2 => FImp (form_subst2 n f1 g) (form_subst2 n f2 g)
+  | FConj f1 f2 => FConj (form_subst2 n f1 g) (form_subst2 n f2 g)
+  | FForallt f => FForallt (form_subst2 n f g)
+  | FForallp f => FForallp (form_subst2 n f g)
+  | FForall2 f => FForall2 (form_subst2 (S n) f (form_lift2 0 g))
+ end.
+
+Definition norm : form := FImp (FImp FBool FBool) FBool.
+
+Definition redcand : form :=
+ FConj
+  (FConj
+   (FForallp (FIn (LApp (LVar 0) (LLVar 0)) 0))
+   (FForallt (FImp (FIn (LMetavar 0) 0) (norm)))
+  )
+  (FForallt (FForallt (FForallp
+   (FImp
+    (FIn (LApp (LMetasubst (LMetavar 1) 0 (LLList [LMetavar 0])) (LLVar 0)) 0)
+    (FIn (LApp (LApp (LAbs (LMetavar 1)) (LLList [LMetavar 0])) (LLVar 0)) 0)
+   )
+  ))).
+
+Fixpoint rc (T : type) : form :=
+ match T with
+  | TVar m => FIn (LMetavar 0) m
+  | TArrow T U => FForallt (FImp (rc T) (form_substt 0 (rc U) (LApp (LMetavar 1) (LLList [LMetavar 0]))))
+  | TForall T => FForall2 (FImp redcand (rc T))
+ end.
+
+Fixpoint form_to_type (f : form) : Type :=
+ match f with
+  | FIn t m => nat
+  | FBool => nat
+  | FImp f g => form_to_type f -> form_to_type g
+  | FConj f g => form_to_type f * form_to_type g
+  | FForallt f => term -> form_to_type f
+  | FForallp f => list term -> form_to_type f
+  | FForall2 f => form_to_type f
+ end.
+Lemma form_to_type_substt : forall (f : form) (n : nat) (t : logterm), form_to_type (form_substt n f t) = form_to_type f.
+intro f; induction f; intros t m; simpl.
+reflexivity.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+(*Lemma form_to_type_liftt : forall (f : form) (n : nat), form_to_type (form_liftt n f) = form_to_type f.
+intro f; induction f; intro m; simpl.
+reflexivity.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+Lemma form_to_type_liftp : forall (f : form) (n : nat), form_to_type (form_liftp n f) = form_to_type f.
+intro f; induction f; intro m; simpl.
+reflexivity.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.*)
+Lemma form_to_type_lift2 : forall (f : form) (n : nat), form_to_type (form_lift2 n f) = form_to_type f.
+intro f; induction f; intro m; simpl.
+destruct (n <? m); reflexivity.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf1; rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+Lemma form_to_type_subst2 : forall (f : form) (n : nat) (g : form) (h : form), form_to_type g = form_to_type h -> form_to_type (form_subst2 n f g) = form_to_type (form_subst2 n f h).
+intro f; induction f; intros m g h Heq; simpl.
+destruct (n ?= m); try reflexivity.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+assumption.
+reflexivity.
+rewrite (IHf1 _ _ _ Heq); rewrite (IHf2 _ _ _ Heq).
+reflexivity.
+rewrite (IHf1 _ _ _ Heq); rewrite (IHf2 _ _ _ Heq).
+reflexivity.
+rewrite (IHf _ g h).
+reflexivity.
+apply Heq.
+rewrite (IHf _ g h).
+reflexivity.
+apply Heq.
+rewrite (IHf _ (form_lift2 0 g) (form_lift2 0 h)).
+reflexivity.
+rewrite form_to_type_lift2.
+rewrite form_to_type_lift2.
+apply Heq.
+Qed.
+Lemma form_to_type_subst2_substt : forall (f : form) (n : nat) (i : nat) (t : logterm) (g : form), form_to_type (form_subst2 n (form_substt i f t) g) = form_to_type (form_subst2 n f g).
+intro f; induction f; intros m i t g; simpl.
+destruct (n ?= m); try reflexivity.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+Lemma form_to_type_subst2_substp : forall (f : form) (n : nat) (i : nat) (p : logtermlist) (g : form), form_to_type (form_subst2 n (form_substp i f p) g) = form_to_type (form_subst2 n f g).
+intro f; induction f; intros m i t g; simpl.
+destruct (n ?= m); try reflexivity.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+Lemma form_to_type_subst2_fin : forall (f : form) (n : nat) (m : nat) (t : logterm), form_to_type (form_subst2 n f (FIn t m)) = form_to_type f.
+intro f; induction f; intros m i t; simpl.
+destruct (n ?= m); reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+(*Lemma form_to_type_subst2_fin2 : forall (f : form) (n : nat) (t : logterm), form_to_type (form_subst2 n (FIn t n) f) = form_to_type f.
+intros f n t; simpl.
+rewrite Nat.compare_refl.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.*)
+
+Fixpoint form_measure (f : form) : nat :=
+ match f with
+  | FIn t m => 0
+  | FBool => 0
+  | FImp f1 f2 => S ((form_measure f1) + (form_measure f2))
+  | FConj f1 f2 => S ((form_measure f1) + (form_measure f2))
+  | FForallt f => S (form_measure f)
+  | FForallp f => S (form_measure f)
+  | FForall2 f => S (form_measure f)
+ end.
+Lemma form_measure_substt : forall (f : form) (n : nat) (t : logterm), form_measure (form_substt n f t) = form_measure f.
+intro f; induction f; intros m t; simpl.
+reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+Lemma form_measure_substp : forall (f : form) (n : nat) (p : logtermlist), form_measure (form_substp n f p) = form_measure f.
+intro f; induction f; intros m t; simpl.
+reflexivity.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf1.
+rewrite IHf2.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+rewrite IHf.
+reflexivity.
+Qed.
+
+Program Fixpoint repl (n : nat) (f : form) {g h : form} (real : form_to_type (FForallt (FConj (FImp g h) (FImp h g)))) {measure (form_measure f)}
+ : form_to_type (FConj (FImp (form_subst2 n f g) (form_subst2 n f h)) (FImp (form_subst2 n f h) (form_subst2 n f g))) :=
+ match f with
+  | FIn t m =>
+   match m ?= n as c
+   return
+    let subst := fun f : form => match c with Eq => form_substt 0 f t | Lt => FIn t m | Gt => FIn t (pred m) end in
+    form_to_type (FConj (FImp (subst g) (subst h)) (FImp (subst h) (subst g)))
+   with
+    | Eq =>
+     let r := real (logterm_to_term t) in
+     (fun y => rew [id] _ in fst r (rew [id] _ in y), fun y => rew [id] _ in snd r (rew [id] _ in y))
+    | _ => (id, id)
+   end
+  | FBool => (id, id)
+  | FImp f1 f2 =>
+   let (r11, r12) := repl n f1 real in
+   let (r21, r22) := repl n f2 real in
+   (fun y z => r21 (y (r12 z)), fun y z => r22 (y (r11 z)))
+  | FConj f1 f2 =>
+   let (r11, r12) := repl n f1 real in
+   let (r21, r22) := repl n f2 real in
+   (fun y => (r11 (fst y), r21 (snd y)), fun y => (r12 (fst y), r22 (snd y)))
+  | FForallt f =>
+   (fun y t => rew [id] _ in fst (repl n (form_substt 0 f (term_to_logterm t)) real) (rew [id] _ in (y t)),
+    fun y t => rew [id] _ in snd (repl n (form_substt 0 f (term_to_logterm t)) real) (rew [id] _ in (y t)))
+  | FForallp f =>
+   (fun y p => rew [id] _ in fst (repl n (form_substp 0 f (termlist_to_logtermlist p)) real) (rew [id] _ in y p),
+    fun y p => rew [id] _ in snd (repl n (form_substp 0 f (termlist_to_logtermlist p)) real) (rew [id] _ in y p))
+  | FForall2 f =>
+   let r := repl (S n) f real in
+     (fun y => rew [id] _ in fst r (rew [id] _ in y), fun y => rew [id] _ in snd r (rew [id] _ in y))
+ end.
+Next Obligation.
+apply form_to_type_substt.
+Qed.
+Next Obligation.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+apply form_to_type_substt.
+Qed.
+Next Obligation.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+fold (m ?= n).
+destruct (m ?= n); reflexivity.
+Qed.
+Next Obligation.
+fold (m ?= n).
+destruct (m ?= n); reflexivity.
+Qed.
+Next Obligation.
+fold (m ?= n).
+destruct (m ?= n); reflexivity.
+Qed.
+Next Obligation.
+fold (m ?= n).
+destruct (m ?= n); reflexivity.
+Qed.
+Next Obligation.
+simpl.
+apply le_lt_n_Sm.
+apply le_plus_l.
+Qed.
+Next Obligation.
+simpl.
+apply le_lt_n_Sm.
+apply le_plus_r.
+Qed.
+Next Obligation.
+simpl.
+apply le_lt_n_Sm.
+apply le_plus_l.
+Qed.
+Next Obligation.
+simpl.
+apply le_lt_n_Sm.
+apply le_plus_r.
+Qed.
+Next Obligation.
+simpl.
+rewrite form_measure_substt.
+constructor.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substt.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substt.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+simpl.
+rewrite form_measure_substt.
+constructor.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substt.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substt.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+simpl.
+rewrite form_measure_substp.
+constructor.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substp.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substp.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+simpl.
+rewrite form_measure_substp.
+constructor.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substp.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_subst2_substp.
+apply form_to_type_subst2.
+reflexivity.
+Qed.
+Next Obligation.
+apply form_to_type_subst2.
+apply form_to_type_lift2.
+Qed.
+Next Obligation.
+apply form_to_type_subst2.
+rewrite form_to_type_lift2.
+reflexivity.
+Qed.
+Next Obligation.
+apply form_to_type_subst2.
+apply form_to_type_lift2.
+Qed.
+Next Obligation.
+apply form_to_type_subst2.
+rewrite form_to_type_lift2.
+reflexivity.
+Qed.
+
+Fixpoint dne (f : form) : ((form_to_type f -> nat) -> nat) -> form_to_type f :=
+ match f with
+  | FIn t n => fun x => x id
+  | FBool => fun x => x id
+  | FImp f g => fun x y => dne g (fun z => x (fun u => z (u y)))
+  | FConj f g => fun x => (dne f (fun y => x (fun z => y (fst z))), dne g (fun y => x (fun z => y (snd z))))
+  | FForallt f => fun x y => dne f (fun z => x (fun u => z (u y)))
+  | FForallp f => fun x y => dne f (fun z => x (fun u => z (u y)))
+  | FForall2 f => dne f
+ end.
+Definition exf (f : form) : nat -> form_to_type f := fun x => dne f (fun y => x).
+
+Parameter brec : forall A : Type, ((A -> nat) -> A) -> ((term -> A) -> nat) -> (term -> option A) -> nat.
+Extract Constant brec => "
+ fun f g ->
+  let rec brec_aux s =
+   g (fun t -> match s t with Some a -> a | None -> f (fun a -> brec_aux (fun u -> if term_equal u t then Some a else s u))) in
+  brec_aux
+ ".
+Definition equiv (f : form) : form := FConj (FImp (FIn (LVar 0) 0) f) (FImp f (FIn (LVar 0) 0)).
+Definition comp (f : form) : form_to_type (FImp (FForall2 (FImp (FForallt (equiv f)) FBool)) FBool) :=
+ fun y => brec (form_to_type (equiv f)) (fun x => exf (equiv f) (x (exf f, fun u => x (fun v => u, fun v => 0)))) y (fun t => None).
+Program Definition elim (f : form) (g : form) : form_to_type (FImp (FForall2 f) (form_subst2 0 f g)) :=
+ fun x => dne (form_subst2 0 f g) (fun y => comp g (fun z => y (fst (repl 0 f z) (rew [id] _ in x)))).
+Next Obligation.
+rewrite form_to_type_subst2_fin.
+reflexivity.
+Qed.
+
+Definition normrc : form_to_type (form_subst2 0 redcand norm) :=
+ (fun p x => x 0, fun t x => x, fun t u p x y => x (fun i => y (S i))).
+
+Program Fixpoint isrc (tcontext : list (form_to_type redcand)) (T : type) : form_to_type (form_subst2 0 redcand (rc T)) :=
+ match T return form_to_type (form_subst2 0 redcand (rc T)) with
+  | TVar m => rew [id] _ in nth m tcontext (exf redcand 0)
+  | TArrow T1 T2 =>
+   let '(isrc11, isrc12, isrc13) := isrc tcontext T1 in
+   let '(isrc21, isrc22, isrc23) := isrc tcontext T2 in
+   (fun p t x => rew [id] _ in isrc21 (t::p),
+    fun t x => isrc22 (App t (Var 0)) (rew [id] _ in x (Var 0) (rew [id] _ in isrc11 [])),
+    fun t u p x v y => rew [id] _ in isrc23 t u (v::p) (rew [id] _ in x v (rew [id] _ in y)))
+  | TForall T =>
+   (fun p x => fst (fst (isrc (x::tcontext) T)) p,
+    fun t x => elim (FImp redcand (FForallt (FImp (rc T) norm))) norm (fun y => rew [id] _ in snd (fst (isrc (y::tcontext) T))) normrc t (rew [id] _ in elim (FImp redcand (rc T)) norm (rew [id] _ in x) normrc),
+    fun t u p y x => snd (isrc (x::tcontext) T) t u p (y x))
+ end.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Defined.
+Next Obligation.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+
+Program Fixpoint adeq (context : list (term * {T : type & form_to_type (rc T)})) (tcontext : list (form_to_type redcand)) (t : fterm) (H : type_correct (map (fun a => projT1 (snd a)) context) t) : form_to_type (rc (type_get (map (fun a => projT1 (snd a)) context) t)) :=
+ match t with
+  | FVar n => rew [id] _ in projT2 (snd (nth n context (Var 0, existT _ (TVar 0) 0)))
+  | FAbs T t =>
+   fun u y =>
+    let context := (u, existT _ T y)::context in
+    rew [id] _ in snd (isrc tcontext (type_get (map (fun a => projT1 (snd a)) context) t)) (term_subst 1 (fterm_to_term t) (map (fun a => term_lift 0 (fst a)) context)) u [] (rew [id] _ in adeq context tcontext t _)
+  | FApp t u => (rew [id] _ in adeq context tcontext t _) (term_subst 0 (fterm_to_term u) (map (fun a => fst a) context)) (adeq context tcontext u _)
+  | FTAbs t => fun x => rew [id] _ in adeq (map (fun a => (fst a, existT _ (type_lift 0 (projT1 (snd a))) (rew [id] _ in projT2 (snd a)))) context) (x::tcontext) t _
+  | FTApp t T =>
+   let U := match type_get (map (fun a => projT1 (snd a)) context) t with TForall U => U | _ => TVar 0 end in
+   rew [id] _ in elim (FImp redcand (form_substt 0 (rc U) (term_to_logterm (term_subst 0 (fterm_to_term t) (map (fun a => fst a) context))))) (rc T) (rew [id] _ in adeq context tcontext t _) (isrc tcontext T)
+ end.
+Next Obligation.
+revert n H.
+induction context; intros n H.
+rewrite nth_overflow; [ | apply le_0_n ].
+rewrite nth_overflow; [ | apply le_0_n ].
+reflexivity.
+rewrite map_cons.
+destruct n.
+reflexivity.
+simpl nth.
+apply IHcontext.
+simpl type_correct in *.
+apply lt_S_n.
+apply H.
+Qed.
+Next Obligation.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+apply H.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+destruct H0.
+destruct H1.
+destruct (type_get _ t); try discriminate.
+simpl.
+rewrite form_to_type_substt.
+injection H1 as H11 H12.
+rewrite <- H11.
+reflexivity.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+destruct H0.
+apply H0.
+Qed.
+Next Obligation.
+simpl; clear.
+generalize 0.
+induction s; simpl; intro m.
+destruct (n <? m); reflexivity.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite <- IHs1.
+rewrite <- IHs2.
+reflexivity.
+rewrite <- IHs.
+reflexivity.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+rewrite map_map.
+simpl.
+rewrite map_map in H.
+apply H.
+Qed.
+Next Obligation.
+rewrite map_map.
+rewrite map_map.
+reflexivity.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+apply H.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+destruct H0.
+rewrite H0.
+simpl.
+rewrite form_to_type_substt.
+reflexivity.
+Qed.
+Next Obligation.
+simpl type_correct in H.
+destruct H.
+destruct H0.
+rewrite H0.
+rewrite form_to_type_subst2_substt.
+clear; revert T.
+generalize 0.
+clear; induction x; intros m T.
+simpl.
+destruct (n ?= m); simpl.
+rewrite form_to_type_substt.
+reflexivity.
+reflexivity.
+reflexivity.
+simpl.
+rewrite IHx1.
+rewrite form_to_type_substt.
+rewrite form_to_type_subst2_substt.
+rewrite IHx2.
+reflexivity.
+simpl.
+rewrite (form_to_type_subst2 _ _ _ (rc T)).
+rewrite IHx.
+assert (forall a b c, b = c -> (a -> b) = (a -> c)).
+intros a b c Heq; rewrite Heq; reflexivity.
+apply H; clear H.
+generalize (S m); clear.
+revert T; induction x; intros T m.
+simpl.
+destruct (n ?= m).
+generalize 0; clear; induction T; intro m.
+simpl.
+destruct (n <? m); reflexivity.
+simpl.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite <- IHT1.
+rewrite <- IHT2.
+reflexivity.
+simpl.
+rewrite <- IHT.
+reflexivity.
+reflexivity.
+reflexivity.
+simpl.
+rewrite form_to_type_substt.
+rewrite form_to_type_substt.
+rewrite <- IHx1.
+rewrite <- IHx2.
+reflexivity.
+simpl.
+rewrite <- IHx.
+rewrite <- IHx.
+rewrite <- IHx.
+reflexivity.
+rewrite form_to_type_lift2.
+reflexivity.
+Qed.
+
+Program Definition bound (t : fterm) (H : type_correct [] t) : nat :=
+ snd (fst (isrc [] (type_get [] t))) (fterm_to_term t) (adeq [] [] t _) id.
+Next Obligation.
+Admitted.
+
+
+Extract Inductive unit => "unit" [ "()" ].
+Extract Inductive bool => "bool" [ "true" "false" ].
+Extract Inductive list => "list" [ "[]" "(::)" ].
+Extract Inductive prod => "(*)"  [ "(,)" ].
+Extract Inductive option => "option"  [ "Some" "None" ].
+Extraction "f.ml" term_equal bound term1 term2.