diff --git a/lang/lifting/src/fv.rs b/lang/lifting/src/fv.rs
index 9566857fc..c44cab51f 100644
--- a/lang/lifting/src/fv.rs
+++ b/lang/lifting/src/fv.rs
@@ -86,19 +86,22 @@ impl FV for ust::Match {
 }
 
 impl FV for ust::Case {
-    fn visit_fv(&self, _v: &mut USTVisitor) {
-        let ust::Case { info: _, name: _, args: _, body: _ } = self;
+    fn visit_fv(&self, v: &mut USTVisitor) {
+        let ust::Case { info: _, name: _, args, body } = self;
 
-        //body.visit_fv(v);
-        // TODO: The visitor context must be extended somehow.
+        v.bind_iter(args.params.iter(), |v| {
+            body.visit_fv(v);
+        })
     }
 }
 
 impl FV for ust::Motive {
     fn visit_fv(&self, v: &mut USTVisitor) {
         let ust::Motive { info: _, param, ret_typ } = self;
+
         param.visit_fv(v);
-        ret_typ.visit_fv(v);
+
+        v.bind_single(param, |v| ret_typ.visit_fv(v))
     }
 }
 
@@ -123,9 +126,8 @@ impl<T: FV> FV for Rc<T> {
 
 impl<T: FV> FV for Option<T> {
     fn visit_fv(&self, v: &mut USTVisitor) {
-        match self {
-            None => {}
-            Some(x) => x.visit_fv(v),
+        if let Some(x) = self {
+            x.visit_fv(v)
         }
     }
 }
diff --git a/lang/syntax/src/ctx/mod.rs b/lang/syntax/src/ctx/mod.rs
index 630b2e075..8a039ff0f 100644
--- a/lang/syntax/src/ctx/mod.rs
+++ b/lang/syntax/src/ctx/mod.rs
@@ -3,9 +3,7 @@ mod levels;
 mod map;
 pub mod map_idx;
 pub mod values;
-mod visit;
 
 pub use def::*;
 pub use levels::*;
 pub use map::*;
-pub use visit::*;
diff --git a/lang/syntax/src/ctx/visit.rs b/lang/syntax/src/ctx/visit.rs
deleted file mode 100644
index 668c74e7b..000000000
--- a/lang/syntax/src/ctx/visit.rs
+++ /dev/null
@@ -1,101 +0,0 @@
-use std::rc::Rc;
-
-use crate::ctx::*;
-use crate::generic::*;
-use codespan::Span;
-
-pub trait VisitCtxExt<P: Phase> {
-    fn ctx_visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2)
-    where
-        P: 'a,
-        I: IntoIterator<Item = &'a Param<P>>,
-        F1: Fn(&mut Self, &'a Param<P>),
-        F2: FnOnce(&mut Self);
-
-    fn ctx_visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2)
-    where
-        P: 'a,
-        I: IntoIterator<Item = &'a ParamInst<P>>,
-        F1: Fn(&mut Self, &'a ParamInst<P>),
-        F2: FnOnce(&mut Self);
-
-    fn ctx_visit_motive_param<X, F>(&mut self, param: &ParamInst<P>, f_inner: F) -> X
-    where
-        F: FnOnce(&mut Self, &ParamInst<P>) -> X;
-
-    fn ctx_visit_self_param<X, F>(
-        &mut self,
-        info: &Option<Span>,
-        name: &Option<Ident>,
-        typ: &TypApp<P>,
-        f_inner: F,
-    ) -> X
-    where
-        F: FnOnce(&mut Self) -> X;
-}
-
-impl<P: Phase, C: BindContext> VisitCtxExt<P> for C
-where
-    for<'a> &'a Param<P>: ContextElem<C::Ctx>,
-    for<'a> &'a ParamInst<P>: ContextElem<C::Ctx>,
-{
-    fn ctx_visit_telescope<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2)
-    where
-        P: 'a,
-        I: IntoIterator<Item = &'a Param<P>>,
-        F1: Fn(&mut Self, &'a Param<P>),
-        F2: FnOnce(&mut Self),
-    {
-        self.bind_fold(
-            params.into_iter(),
-            Vec::new(),
-            |this, mut params_out, param| {
-                f_acc(this, param);
-                params_out.push(());
-                params_out
-            },
-            |this, _params| f_inner(this),
-        )
-    }
-
-    fn ctx_visit_telescope_inst<'a, I, F1, F2>(&mut self, params: I, f_acc: F1, f_inner: F2)
-    where
-        P: 'a,
-        I: IntoIterator<Item = &'a ParamInst<P>>,
-        F1: Fn(&mut Self, &'a ParamInst<P>),
-        F2: FnOnce(&mut Self),
-    {
-        self.bind_fold(
-            params.into_iter(),
-            Vec::new(),
-            |this, mut params_out, param| {
-                f_acc(this, param);
-                params_out.push(());
-                params_out
-            },
-            |this, _params| f_inner(this),
-        )
-    }
-
-    fn ctx_visit_motive_param<X, F>(&mut self, param: &ParamInst<P>, f_inner: F) -> X
-    where
-        F: FnOnce(&mut Self, &ParamInst<P>) -> X,
-    {
-        self.bind_single(param, |ctx| f_inner(ctx, param))
-    }
-
-    fn ctx_visit_self_param<X, F>(
-        &mut self,
-        _info: &Option<Span>,
-        name: &Option<Ident>,
-        typ: &TypApp<P>,
-        f_inner: F,
-    ) -> X
-    where
-        F: FnOnce(&mut Self) -> X,
-    {
-        let param = Param { name: name.clone().unwrap_or_default(), typ: Rc::new(typ.to_exp()) };
-
-        self.bind_single(&param, |ctx| f_inner(ctx))
-    }
-}