diff --git a/_CoqProject b/_CoqProject
index f1b98b3..0de81a5 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -25,7 +25,7 @@ theories/DirectedDirections.v
 theories/DirectedContext.v
 theories/DirectedDirectioning.v
 theories/DirectedSemantics.v
-
+theories/DirectedDeclarativeTyping.v
 
 theories/LogicalRelation.v
 theories/LogicalRelation/Induction.v
diff --git a/theories/DirectedSemantics.v b/theories/DirectedSemantics.v
index cd44c74..8657444 100644
--- a/theories/DirectedSemantics.v
+++ b/theories/DirectedSemantics.v
@@ -3,8 +3,8 @@ From Coq Require Import ssreflect.
 From Equations Require Import Equations.
 From smpl Require Import Smpl.
 From LogRel.AutoSubst Require Import core unscoped Ast Extra.
-From LogRel Require Import DirectedDirections DirectedContext DirectedDirectioning DirectedDeclarativeTyping.
 From LogRel Require Import Utils BasicAst.
+From LogRel Require Import DirectedDirections DirectedContext DirectedDirectioning.
 
 Reserved Notation "[ Δ |- w : t -( d )- u : A ]" (at level 0, Δ, d, t, u, A, w at level 50).
 Reserved Notation "[ Δ |- ϕ : σ -( )- τ : Θ ]" (at level 0, Δ, Θ, σ, τ, ϕ at level 50).
@@ -113,6 +113,8 @@ Section MorphismDefinition.
 
   where "[ Δ |- w : t -( d )- u : A ]" := (TermRel Δ t u d A w).
 
+  Close Scope typing_scope.
+
   Context (type_act : forall (γ : list direction) (dA : direction) (A : term) (wdA : [γ |- A ◃ dA]) (σ τ : nat -> term) (φ : list term), term).
 
   (* Given a context of directions γ coming from Θ,
diff --git a/theories/DirectedTyping.v b/theories/DirectedTyping.v
index d68560c..966a812 100644
--- a/theories/DirectedTyping.v
+++ b/theories/DirectedTyping.v
@@ -284,6 +284,9 @@ Module Examples.
 
     Definition ctx := εᵈ ,, Fun \ U @ Discr ,, Cofun \ tProd (tRel 0) U @ Cofun.
     
+    [ Θ |-(Fun) A ]
+    [ Θ ,, Discr \ A @ Fun |-(Cofun) B ]
+    
     Definition sup_ctx 
       (* tW should bind one variable in its second argument *)
       (tW : term -> term -> term) :=