diff --git a/src/kind-checker/src/compiler/mod.rs b/src/kind-checker/src/compiler/mod.rs
index 6089b026..c20b1946 100644
--- a/src/kind-checker/src/compiler/mod.rs
+++ b/src/kind-checker/src/compiler/mod.rs
@@ -134,7 +134,7 @@ fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, exp
                 lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body)),
             ],
         ),
-        Lambda(name, body) => mk_quoted_ctr(
+        Lambda(name, body, erased) => mk_quoted_ctr(
             eval_ctr(quote, TermTag::Lambda),
             vec![span_to_num(expr.span), mk_u60(name.encode()), lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body))],
         ),
diff --git a/src/kind-checker/src/report.rs b/src/kind-checker/src/report.rs
index 24890c81..830ad2c1 100644
--- a/src/kind-checker/src/report.rs
+++ b/src/kind-checker/src/report.rs
@@ -86,6 +86,7 @@ fn parse_all_expr(names: im::HashMap<String, String>, term: &Term) -> Result<Box
                 parse_orig(&args[0])?,
                 Ident::generate(&parse_name(&args[1])?),
                 parse_all_expr(names, &args[2])?,
+                false // TODO: Fix
             )),
             "Kind.Quoted.let" => Ok(Expr::let_(
                 parse_orig(&args[0])?,
diff --git a/src/kind-derive/src/open.rs b/src/kind-derive/src/open.rs
index 5e2cf097..ff7b0833 100644
--- a/src/kind-derive/src/open.rs
+++ b/src/kind-derive/src/open.rs
@@ -7,7 +7,7 @@ use kind_tree::concrete::*;
 use kind_tree::concrete::{self};
 use kind_tree::symbol::{Ident, QualifiedIdent};
 
-pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
+pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
     let mk_var = |name: Ident| -> Box<Expr> {
         Box::new(Expr {
             data: ExprKind::Var(name),
@@ -36,19 +36,19 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
         })
     };
 
-    let name = sum.name.add_segment("open");
+    let name = rec.name.add_segment("open");
 
     let mut types = Telescope::default();
 
-    for arg in sum.parameters.iter() {
+    for arg in rec.parameters.iter() {
         types.push(arg.to_implicit())
     }
 
     // The type
 
-    let all_args = sum.parameters.clone();
+    let all_args = rec.parameters.clone();
     let res_motive_ty = mk_cons(
-        sum.name.clone(),
+        rec.name.clone(),
         all_args
             .iter()
             .cloned()
@@ -66,7 +66,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
 
     let cons_tipo = mk_var(Ident::generate("_res"));
 
-    let cons_type = sum.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| {
+    let cons_type = rec.fields.iter().rfold(cons_tipo, |out, (name, _, typ)| {
         mk_pi(name.clone(), typ.clone(), out)
     });
 
@@ -94,7 +94,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
 
     let mut pats: Vec<Box<Pat>> = Vec::new();
 
-    let spine: Vec<Ident> = sum
+    let spine: Vec<Ident> = rec
         .fields
         .iter()
         .map(|(name, _, _)| name.with_name(|f| format!("{}_", f)))
@@ -102,7 +102,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
 
     pats.push(Box::new(Pat {
         data: concrete::pat::PatKind::App(
-            sum.name.add_segment(sum.constructor.to_str()),
+            rec.name.add_segment(rec.constructor.to_str()),
             spine
                 .iter()
                 .cloned()
@@ -137,7 +137,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
         range,
     })];
 
-    Entry {
+    let entry = Entry {
         name,
         docs: Vec::new(),
         args: types,
@@ -145,5 +145,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry {
         rules,
         range,
         attrs: Vec::new(),
-    }
+    };
+
+    entry
 }
diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs
index 4668062c..9a2b3488 100644
--- a/src/kind-parser/src/expr.rs
+++ b/src/kind-parser/src/expr.rs
@@ -133,7 +133,7 @@ impl<'a> Parser<'a> {
         let end_range = expr.range;
 
         Ok(Box::new(Expr {
-            data: ExprKind::Lambda(ident, None, expr),
+            data: ExprKind::Lambda(ident, None, expr, false),
             range: name_span.mix(end_range),
         }))
     }
@@ -152,7 +152,7 @@ impl<'a> Parser<'a> {
             let body = self.parse_expr(false)?;
             Ok(Box::new(Expr {
                 range: range.mix(body.range),
-                data: ExprKind::Lambda(ident, Some(typ), body),
+                data: ExprKind::Lambda(ident, Some(typ), body, false),
             }))
         } else if self.check_and_eat(Token::RightArrow) {
             let body = self.parse_expr(false)?;
@@ -384,15 +384,16 @@ impl<'a> Parser<'a> {
 
     fn parse_app_binding(&mut self) -> Result<AppBinding, SyntaxError> {
         self.ignore_docs();
-        let (erased, data) = if self.get().same_variant(&Token::LBrace) {
+        let (erased, data) = /*if self.get().same_variant(&Token::LBrace) {
             let start = self.range();
             self.advance(); // '{'
-            let atom = self.parse_expr(true)?;
+            let atom = self.parse_atom()?;
             self.eat_closing_keyword(Token::RBrace, start)?;
             (true, atom)
-        } else {
-            (false, self.parse_expr(false)?)
-        };
+        } else {*/
+            (false, self.parse_atom()?)
+        // }
+        ;
         Ok(AppBinding { data, erased })
     }
 
@@ -594,6 +595,7 @@ impl<'a> Parser<'a> {
         self.advance(); // 'match'
 
         let typ = self.parse_upper_id()?;
+
         let scrutinizer = self.parse_expr(false)?;
 
         self.eat_variant(Token::LBrace)?;
diff --git a/src/kind-pass/src/desugar/destruct.rs b/src/kind-pass/src/desugar/destruct.rs
index d54a318c..03a69983 100644
--- a/src/kind-pass/src/desugar/destruct.rs
+++ b/src/kind-pass/src/desugar/destruct.rs
@@ -69,6 +69,7 @@ impl<'a> DesugarState<'a> {
         match binding {
             Destruct::Destruct(_, typ, case, jump_rest) => {
                 let entry = self.old_book.entries.get(&typ.to_string());
+                let count = self.old_book.count.get(&typ.to_string()).unwrap();
 
                 let record = if let Some(TopLevel::RecordType(record)) = entry {
                     record
@@ -100,9 +101,11 @@ impl<'a> DesugarState<'a> {
 
                 let open_id = typ.add_segment("open");
 
+                let irrelev = count.arguments.map(|x| x.erased).to_vec();
+
                 let spine = vec![
                     val,
-                    desugared::Expr::unfold_lambda(range, &arguments, next(self)),
+                    desugared::Expr::unfold_lambda(range, &irrelev, &arguments, next(self)),
                 ];
 
                 self.mk_desugared_fun(range, open_id, spine, false)
@@ -174,6 +177,7 @@ impl<'a> DesugarState<'a> {
                 self.send_err(PassError::DuplicatedNamed(range, case.constructor.range));
             } else {
                 let sum_c = &sum.constructors[index];
+
                 let ordered = self.order_case_arguments(
                     (&case.constructor.range, case.constructor.to_string()),
                     &sum_c
@@ -204,8 +208,10 @@ impl<'a> DesugarState<'a> {
         for (i, case_arg) in cases_args.iter().enumerate() {
             let case = &sum.constructors[i];
             if let Some((range, arguments, val)) = &case_arg {
+                let case: Vec<bool> = case.args.iter().map(|x| x.erased).rev().collect();
                 lambdas.push(desugared::Expr::unfold_lambda(
                     *range,
+                    &case,
                     arguments,
                     self.desugar_expr(val),
                 ))
@@ -226,7 +232,7 @@ impl<'a> DesugarState<'a> {
             let mut idx: Vec<Ident> = sum.parameters.extend(&sum.indices).iter().map(|x| x.name.clone()).collect();
             idx.push(Ident::generate("_val"));
             idx.iter().rfold(self.gen_hole_expr(), |expr, l| {
-                desugared::Expr::lambda(l.range, l.clone(), expr)
+                desugared::Expr::lambda(l.range, l.clone(), expr, false)
             })
         };
 
diff --git a/src/kind-pass/src/desugar/expr.rs b/src/kind-pass/src/desugar/expr.rs
index 1b48ac1a..7f567763 100644
--- a/src/kind-pass/src/desugar/expr.rs
+++ b/src/kind-pass/src/desugar/expr.rs
@@ -51,7 +51,7 @@ impl<'a> DesugarState<'a> {
             this.mk_desugared_fun(
                 range,
                 bind_ident.clone(),
-                vec![expr, desugared::Expr::lambda(range, name, next)],
+                vec![expr, desugared::Expr::lambda(range, name, next, false)],
                 false,
             )
         };
@@ -150,7 +150,7 @@ impl<'a> DesugarState<'a> {
 
         let spine = vec![
             self.desugar_expr(typ),
-            desugared::Expr::lambda(range, name, self.desugar_expr(body)),
+            desugared::Expr::lambda(range, name, self.desugar_expr(body), true),
         ];
 
         self.mk_desugared_ctr(range, sigma, spine, false)
@@ -244,8 +244,8 @@ impl<'a> DesugarState<'a> {
                 self.desugar_expr(left),
                 self.desugar_expr(right),
             ),
-            Lambda(ident, _typ, body) => {
-                desugared::Expr::lambda(expr.range, ident.clone(), self.desugar_expr(body))
+            Lambda(ident, _typ, body, erased) => {
+                desugared::Expr::lambda(expr.range, ident.clone(), self.desugar_expr(body), *erased)
             }
             Ann(val, typ) => {
                 desugared::Expr::ann(expr.range, self.desugar_expr(val), self.desugar_expr(typ))
diff --git a/src/kind-pass/src/desugar/top_level.rs b/src/kind-pass/src/desugar/top_level.rs
index 375c9e73..535cfe1a 100644
--- a/src/kind-pass/src/desugar/top_level.rs
+++ b/src/kind-pass/src/desugar/top_level.rs
@@ -266,9 +266,7 @@ impl<'a> DesugarState<'a> {
                     // inductive types can be used in patterns.
                 }
 
-                let (hidden, _erased) = entry.arguments.count_implicits();
-
-                let fill_hidden = spine.len() == entry.arguments.len() - hidden;
+                let fill_hidden = spine.len() == entry.arguments.len() - entry.hiddens;
 
                 let mut new_spine = Vec::new();
 
@@ -284,12 +282,12 @@ impl<'a> DesugarState<'a> {
                         }
                     }
                 } else if entry.arguments.len() != spine.len() {
-                    println!("{}", pat);
+                    println!("{}: {:?}", head, entry);
                     self.send_err(PassError::IncorrectArity(
                         head.range,
                         spine.iter().map(|x| x.range).collect(),
                         entry.arguments.len(),
-                        hidden,
+                        entry.hiddens,
                     ));
                     return desugared::Expr::err(pat.range);
                 } else {
diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs
index 99994489..15dde7bb 100644
--- a/src/kind-pass/src/erasure/mod.rs
+++ b/src/kind-pass/src/erasure/mod.rs
@@ -305,16 +305,24 @@ impl<'a> ErasureState<'a> {
 
                 Box::new(expr.clone())
             }
-            Lambda(name, body) => {
+            Lambda(name, body, erased) => {
                 let ctx = self.ctx.clone();
-                self.ctx.insert(name.to_string(), (name.range, *on));
+                if *erased {
+                    self.ctx.insert(name.to_string(), (name.range, (Some(name.range), Relevance::Irrelevant)));
+                } else {
+                    self.ctx.insert(name.to_string(), (name.range, *on));
+                }
                 let body = self.erase_expr(on, body);
                 self.ctx = ctx;
 
-                Box::new(Expr {
-                    span: expr.span,
-                    data: ExprKind::Lambda(name.clone(), body),
-                })
+                if *erased {
+                    body
+                } else {
+                    Box::new(Expr {
+                        span: expr.span,
+                        data: ExprKind::Lambda(name.clone(), body, *erased),
+                    })
+                }
             }
             Let(name, val, body) => {
                 let ctx = self.ctx.clone();
diff --git a/src/kind-pass/src/unbound/mod.rs b/src/kind-pass/src/unbound/mod.rs
index 8230ee63..26996354 100644
--- a/src/kind-pass/src/unbound/mod.rs
+++ b/src/kind-pass/src/unbound/mod.rs
@@ -361,7 +361,7 @@ impl Visitor for UnboundCollector {
                 self.visit_expr(body);
                 self.context_vars.pop();
             }
-            ExprKind::Lambda(ident, binder, body) => {
+            ExprKind::Lambda(ident, binder, body, erased) => {
                 match binder {
                     Some(x) => self.visit_expr(x),
                     None => (),
diff --git a/src/kind-target-hvm/src/lib.rs b/src/kind-target-hvm/src/lib.rs
index c1f0b336..98ec348b 100644
--- a/src/kind-target-hvm/src/lib.rs
+++ b/src/kind-target-hvm/src/lib.rs
@@ -9,7 +9,7 @@ pub fn compile_term(expr: &desugared::Expr) -> Box<Term> {
         Var(name) => Box::new(Term::Var {
             name: name.to_string(),
         }),
-        Lambda(binder, body) => Box::new(Term::Lam {
+        Lambda(binder, body, _erased) => Box::new(Term::Lam {
             name: binder.to_string(),
             body: compile_term(body),
         }),
diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs
index 32ddf907..5fb9f9d6 100644
--- a/src/kind-tree/src/concrete/expr.rs
+++ b/src/kind-tree/src/concrete/expr.rs
@@ -134,7 +134,7 @@ pub enum ExprKind {
     /// The dependent product space (e.g. [x : Int] -> y)
     Sigma(Option<Ident>, Box<Expr>, Box<Expr>),
     /// A anonymous function that receives one argument
-    Lambda(Ident, Option<Box<Expr>>, Box<Expr>),
+    Lambda(Ident, Option<Box<Expr>>, Box<Expr>, bool),
     /// Application of a expression to a spine of expressions
     App(Box<Expr>, Vec<AppBinding>),
     /// Declaration of a local variable
@@ -402,8 +402,10 @@ impl Display for Expr {
                 head,
                 spine.iter().map(|x| format!(" {}", x)).collect::<String>()
             ),
-            Lambda(binder, None, body) => write!(f, "({} => {})", binder, body),
-            Lambda(binder, Some(typ), body) => write!(f, "(({} : {}) => {})", binder, typ, body),
+            Lambda(binder, None, body, false) => write!(f, "({} => {})", binder, body),
+            Lambda(binder, Some(typ), body, false) => write!(f, "(({} : {}) => {})", binder, typ, body),
+            Lambda(binder, None, body, true) => write!(f, "({{{}}} => {})", binder, body),
+            Lambda(binder, Some(typ), body, true) => write!(f, "({{{} : {}}} => {})", binder, typ, body),
             Pair(fst, snd) => write!(f, "($ {} {})", fst, snd),
             App(head, spine) => write!(
                 f,
diff --git a/src/kind-tree/src/concrete/mod.rs b/src/kind-tree/src/concrete/mod.rs
index f1a2b0e8..ebbe9262 100644
--- a/src/kind-tree/src/concrete/mod.rs
+++ b/src/kind-tree/src/concrete/mod.rs
@@ -548,13 +548,13 @@ impl RecordDecl {
     }
 
     pub fn extract_book_info_of_constructor(&self) -> EntryMeta {
-        let mut arguments = Telescope::default();
+        let mut arguments;
         let mut hiddens = 0;
         let mut erased = 0;
 
-        hiddens += self.parameters.0.len();
-        erased += self.parameters.0.len();
-        arguments = arguments.extend(&self.parameters);
+        hiddens += self.parameters.len();
+        erased += self.parameters.len();
+        arguments = self.parameters.map(|x| x.to_implicit());
 
         let field_args: Vec<Argument> = self
             .fields
diff --git a/src/kind-tree/src/concrete/visitor.rs b/src/kind-tree/src/concrete/visitor.rs
index 6fffb576..2c404c5c 100644
--- a/src/kind-tree/src/concrete/visitor.rs
+++ b/src/kind-tree/src/concrete/visitor.rs
@@ -411,7 +411,7 @@ pub fn walk_expr<T: Visitor>(ctx: &mut T, expr: &mut Expr) {
             ctx.visit_qualified_ident(ident);
             ctx.visit_sttm(sttm)
         }
-        ExprKind::Lambda(ident, binder, body) => {
+        ExprKind::Lambda(ident, binder, body, _erased) => {
             ctx.visit_ident(ident);
             match binder {
                 Some(x) => ctx.visit_expr(x),
diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs
index 8bced2e4..2477e917 100644
--- a/src/kind-tree/src/desugared/mod.rs
+++ b/src/kind-tree/src/desugared/mod.rs
@@ -30,7 +30,7 @@ pub enum ExprKind {
     /// The dependent function space (e.g. (x : Int) -> y)
     All(Ident, Box<Expr>, Box<Expr>),
     /// A anonymous function that receives one argument
-    Lambda(Ident, Box<Expr>),
+    Lambda(Ident, Box<Expr>, bool),
     /// Application of a expression to a spine of expressions
     App(Box<Expr>, Vec<AppBinding>),
     /// Application of a function
@@ -98,25 +98,26 @@ impl Expr {
         })
     }
 
-    pub fn lambda(range: Range, ident: Ident, body: Box<Expr>) -> Box<Expr> {
+    pub fn lambda(range: Range, ident: Ident, body: Box<Expr>, erased: bool) -> Box<Expr> {
         Box::new(Expr {
             span: Span::Locatable(range),
-            data: ExprKind::Lambda(ident, body),
+            data: ExprKind::Lambda(ident, body, erased),
         })
     }
 
     pub fn identity_lambda(ident: Ident) -> Box<Expr> {
         Box::new(Expr {
             span: Span::Generated,
-            data: ExprKind::Lambda(ident.clone(), Self::var(ident)),
+            data: ExprKind::Lambda(ident.clone(), Self::var(ident), false),
         })
     }
 
-    pub fn unfold_lambda(range: Range, idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
+    pub fn unfold_lambda(range: Range, irrelev: &[bool], idents: &[Ident], body: Box<Expr>) -> Box<Expr> {
         idents
             .iter()
             .rev()
-            .fold(body, |body, ident| Expr::lambda(range, ident.clone(), body))
+            .zip(irrelev)
+            .fold(body, |body, (ident, irrelev)| Expr::lambda(range, ident.clone(), body, *irrelev))
     }
 
     pub fn app(range: Range, ident: Box<Expr>, spine: Vec<AppBinding>) -> Box<Expr> {
@@ -334,7 +335,8 @@ impl Display for Expr {
             Num(self::Num::U120(n)) => write!(f, "{}u120", n),
             All(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
             Var(name) => write!(f, "{}", name),
-            Lambda(binder, body) => write!(f, "({} => {})", binder, body),
+            Lambda(binder, body, false) => write!(f, "({} => {})", binder, body),
+            Lambda(binder, body, true) => write!(f, "({{{}}} => {})", binder, body),
             Sub(name, _, redx, expr) => write!(f, "({} ## {}/{})", expr, name, redx),
             App(head, spine) => write!(
                 f,