§ LCNF

let x : Nat := 2
let xarr : Vec Int x := Nil
let 2arr : Vec Int 2 := Nil
in rfl : xarr = 2arr
(\x ->
   let xarr : Vec Int x := Nil
   let 2arr : Vec Int 2 := Nil
   in rfl : xarr = 2arr) 2
      ^^^^^^^^^^^^^^^^^ <---- (ill-typed under CIC)
Erased a ~ Erased b
(\x ->
   let xarr : Vec Int (Erased x) := Nil
   let 2arr : Vec Int (Erased 2) := Nil
   in rfl : xarr = 2arr) 2
      ^^^^^^^^^^^^^^^^^ <---- (ill-typed under CIC)

§ Erased

match x with
  | F1 f1 => h f1
  | F2 f2 => h f2
def tupleN (n: Nat) (t: Type) := 
  match n with
  | 0 => Unit
  | n+1 => t * (tupleN n t)

def foo n := Vec Int n
 
Any ~ t
def f (n: Nat): (tupleN n t) := ...
def f (n: Nat): Any := ...