-----------------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
-----------------------------------------------------------------------------------------
     ( n : Nat ;  X : * !                            ( n ;  x : X ;  xs : Vec n X !
data !------------------!  where (--------------! ;  !----------------------------!
     !   Vec n X : *    )        ! vnil :       !    !      vcons _n x xs :       !
                                 !   Vec zero X )    !        Vec (suc n) X       )
-----------------------------------------------------------------------------------------
     (  n : Nat ;  x : X  !                
let  !--------------------!                
     ! vec _n x : Vec n X )                
                                           
     vec _ n x <= rec n                    
     { vec _ n x <= case n                 
       { vec _ zero x => vnil              
         vec _ (suc n) x => vcons x (vec x)
       }                                   
     }                                     
-----------------------------------------------------------------------------------------
     ( gs : Vec n (S -> T) ;  ss : Vec n S !                         
let  !-------------------------------------!                         
     !        vapp gs ss : Vec n T         )                         
                                                                     
     vapp gs ss <= rec gs                                            
     { vapp gs ss <= case gs                                         
       { vapp vnil ss <= case ss                                     
         { vapp vnil vnil => vnil                                    
         }                                                           
         vapp (vcons g gs) ss <= case ss                             
         { vapp (vcons g gs) (vcons s ss) => vcons (g s) (vapp gs ss)
         }                                                           
       }                                                             
     }                                                               
-----------------------------------------------------------------------------------------
     (      xss : Vec m (Vec n X)      !                                       
let  !---------------------------------!                                       
     ! transpose xss : Vec n (Vec m X) )                                       
                                                                               
     transpose xss <= rec xss                                                  
     { transpose xss <= case xss                                               
       { transpose vnil => vec vnil                                            
         transpose (vcons xs xss) => vapp (vapp (vec vcons) xs) (transpose xss)
       }                                                                       
     }                                                                         
-----------------------------------------------------------------------------------------
     (  x : X   !
let  !----------!
     ! id x : X )
                 
     id x => x   
-----------------------------------------------------------------------------------------
                                     (  S, T : Ty   !
data (--------!  where (--------! ;  !--------------!
     ! Ty : * )        ! N : Ty )    ! Arr S T : Ty )
-----------------------------------------------------------------------------------------
                                     ( Gam : Cx ;  S : Ty !
data (--------!  where (--------! ;  !--------------------!
     ! Cx : * )        ! E : Cx )    !    C Gam S : Cx    )
-----------------------------------------------------------------------------------------
     (   Gam : Cx    !                                    ( Gam                    !
     !               !                                    !                        !
     !   T : Ty      !                                    ! S, T ;  i : Var Gam T  !
data !---------------!  where (----------------------! ;  !------------------------!
     ! Var Gam T : * )        ! vz : Var (C Gam S) S )    ! vs i : Var (C Gam S) T )
-----------------------------------------------------------------------------------------
     ( Gam : Cx ;  T : Ty !                                                             
data !--------------------!                                                             
     !    Tm Gam T : *    )                                                             
                                                                                        
      ( Gam                !    ( f : Tm Gam (Arr S T) !                                
      !                    !    !                      !                                
      ! T ;  i : Var Gam T !    ! s : Tm Gam S         !    (    t : Tm (C Gam S) T    !
where !--------------------! ;  !----------------------! ;  !--------------------------!
      !  var i : Tm Gam T  )    !  app f s : Tm Gam T  )    ! lda t : Tm Gam (Arr S T) )
-----------------------------------------------------------------------------------------
     (             (   i : Var Gam T   !                              !
     ! Gam, Del ;  !-------------------! ;  S, T ;  i : Var (C Gam! T !
     !             ! rho i : Var Del T )                    !% S  )   !
let  !----------------------------------------------------------------!
     !                 weakR rho i : Var (C Del S) T                  )
                                                                       
     weakR rho i <= case i                                             
     { weakR rho vz => vz                                              
       weakR rho (vs i) => vs (rho i)                                  
     }                                                                 
-----------------------------------------------------------------------------------------
     (             (   i : Var Gam T   !                 !
     ! Gam, Del ;  !-------------------! ;  t : Tm Gam S !
     !             ! rho i : Var Del T )                 !
let  !---------------------------------------------------!
     !               ren rho t : Tm Del S                )
                                                          
     ren rho t <= rec t                                   
     { ren rho t <= case t                                
       { ren rho (var i) => var (rho i)                   
         ren rho (app f s) => app (ren rho f) (ren rho s) 
         ren rho (lda t) => lda (ren (weakR rho) t)       
       }                                                  
     }                                                    
-----------------------------------------------------------------------------------------
     (             (  i : Var Gam T   !                              !
     ! Gam, Del ;  !------------------! ;  S, T ;  i : Var (C Gam! T !
     !             ! sig i : Tm Del T )                    !% S  )   !
let  !---------------------------------------------------------------!
     !                 weakS sig i : Tm (C Del S) T                  )
                                                                      
     weakS sig i <= case i                                            
     { weakS sig vz => var vz                                         
       weakS sig (vs i) => ren vs (sig i)                             
     }                                                                
-----------------------------------------------------------------------------------------
     (             (  i : Var Gam T   !                      !
     ! Gam, Del ;  !------------------! ;  S ;  t : Tm Gam S !
     !             ! sig i : Tm Del T )                      !
let  !-------------------------------------------------------!
     !                 sub sig t : Tm Del S                  )
                                                              
     sub sig t <= rec t                                       
     { sub sig t <= case t                                    
       { sub sig (var i) => sig i                             
         sub sig (app f s) => app (sub sig f) (sub sig s)     
         sub sig (lda t) => lda (sub (weakS sig) t)           
       }                                                      
     }                                                        
-----------------------------------------------------------------------------------------
                             ( Thing                                                    !
                             !                                                          !
                             ! ( Gam ;  T ;  i : Var Gam T !                            !
                             ! !---------------------------!                            !
                             ! !    vr i : Thing Gam T     )                            !
                             !                                                          !
                             ! ( Gam                  !    ( Gam                      ! !
                             ! !                      !    !                          ! !
     ( Thing :      !        ! ! T ;  t : Thing Gam T !    ! S, T ;  t : Thing Gam T  ! !
     !   Cx ->      !        ! !----------------------! ;  !--------------------------! !
     !     Ty -> *  !        ! !   tm t : Tm Gam T    )    ! wk t : Thing (C Gam S) T ) !
data !--------------!  where !----------------------------------------------------------!
     ! Gadget Thing !        !              gadget vr tm wk : Gadget Thing              )
     !  : *         )                                                                    
-----------------------------------------------------------------------------------------
     (                                 ( i : Var Gam T !                              !
     ! g : Gadget Thing ;  Gam, Del ;  !---------------! ;  S, T ;  i : Var (C Gam! T !
     !                                 ! tau i :       !                    !% S  )   !
     !                                 !   Thing Del T )                              !
let  !--------------------------------------------------------------------------------!
     !                       weakT g tau i : Thing (C Del S) T                        )
                                                                                       
     weakT g tau i <= case g                                                           
     { weakT (gadget vr tm wk) tau i <= case i                                         
       { weakT (gadget vr tm wk) tau vz => vr vz                                       
         weakT (gadget vr tm wk) tau (vs i) => wk (tau i)                              
       }                                                                               
     }                                                                                 
-----------------------------------------------------------------------------------------
     (                                 (    i : Var Gam T    !                      !
     ! g : Gadget Thing ;  Gam, Del ;  !---------------------! ;  S ;  t : Tm Gam S !
     !                                 ! tau i : Thing Del T )                      !
let  !------------------------------------------------------------------------------!
     !                           trav g tau t : Tm Del S                            )
                                                                                     
     trav g tau t <= rec t                                                           
     { trav g tau t <= case t                                                        
       { trav g tau (var i) <= case g                                                
         { trav (gadget vr tm wk) tau (var i) => tm (tau i)                          
         }                                                                           
         trav g tau (app f s) => app (trav g tau f) (trav g tau s)                   
         trav g tau (lda t) => lda (trav g (weakT g tau) t)                          
       }                                                                             
     }                                                                               
-----------------------------------------------------------------------------------------
let  (------------------!   
     ! REN : Gadget Var )   
                            
     REN => gadget id var vs
-----------------------------------------------------------------------------------------
let  (-----------------!               
     ! SUB : Gadget Tm )               
                                       
     SUB => gadget var id (trav REN vs)
-----------------------------------------------------------------------------------------