diff --git a/client/F.ml b/client/F.ml
index 60f49074d0ae178e04190a94710cce8f026d8b6f..72891b5935d8698d7f9b806e46fdd6e2a24a19b1 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -4,11 +4,20 @@
 
 (* Types. *)
 
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
    we might wish to support them, but also because even if we disallow them,
    they can still arise during unification (the occurs check is run late), so
    we must be able to display them as part of a type error message. *)
 
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+   equality checking, we do not allow ∀ under μ.
+   For instance :
+           ∀ a. μ t. a -> t is allowed
+           μ t . ∀ a . (a -> t) is not allowed
+           μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
 (* Nominal or de Bruijn representation of type variables and binders. The
    nominal representation is more convenient when translating from ML to F,
    while the de Bruijn representation is more convenient when type-checking
@@ -54,7 +63,27 @@ type debruijn_datatype_env =
 
 (* Nominal representation of term variables and binders. *)
 
-type tevar = string
+(* Nominal or de Bruijn representation of type variables and binders. *)
+
+(* We include a term [Refl] that represents a type equality witness.
+   Note that it has only one type argument but is typed as a witness for
+   an equality between two possibly distinct types (see [TyEq] above).
+
+   [Use] is a construct that "opens" a type equality. That is, it allows us to
+   reason in a context where two types are assumed to be equals.
+   It is supposed to be used with a type equality witness as a left-hand side :
+
+           use (eq : TyEq (ty1, ty2)) in
+           ... (* here ty1 and ty2 are assumed to be equal *)
+
+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce
+   a construct [Absurd], that can be used as a placeholder in pieces of code
+   with inconsistent equations in the environment and that are thus
+   unreachable. *)
+
+type tevar =
+  string
 
 type ('a, 'b) term =
   | Var of range *  tevar
diff --git a/client/F.mli b/client/F.mli
index f5e37bf9cf5680bc72e9a29b6e6df1a8838b8420..ee46f38aafc4eacc238ff6d5f8e1e29491a778e9 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -4,11 +4,20 @@
 
 (* Types. *)
 
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
    we might wish to support them, but also because even if we disallow them,
    they can still arise during unification (the occurs check is run late), so
    we must be able to display them as part of a type error message. *)
 
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+   equality checking, we do not allow ∀ under μ.
+   For instance :
+           ∀ a. μ t. a -> t is allowed
+           μ t . ∀ a . (a -> t) is not allowed
+           μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
 (* Nominal or de Bruijn representation of type variables and binders. The
    nominal representation is more convenient when translating from ML to F,
    while the de Bruijn representation is more convenient when type-checking
@@ -56,6 +65,23 @@ type debruijn_datatype_env =
 
 (* Nominal or de Bruijn representation of type variables and binders. *)
 
+(* We include a term [Refl] that represents a type equality witness.
+   Note that it has only one type argument but is typed as a witness for
+   an equality between two possibly distinct types (see [TyEq] above).
+
+   [Use] is a construct that "opens" a type equality. That is, it allows us to
+   reason in a context where two types are assumed to be equals.
+   It is supposed to be used with a type equality witness as a left-hand side :
+
+           use (eq : TyEq (ty1, ty2)) in
+           ... (* here ty1 and ty2 are assumed to be equal *)
+
+   Doing this might introduce inconsistent assumptions about types (this can
+   occur for example inside a pattern matching). That is why we introduce
+   a construct [Absurd], that can be used as a placeholder in pieces of code
+   with inconsistent equations in the environment and that are thus
+   unreachable. *)
+
 type tevar =
     string