------------------------------------------------------------------------------
                                      (   n : Nat   !
data (---------!  where zero : Nat ;  !-------------!
     ! Nat : * )                      ! suc n : Nat )
------------------------------------------------------------------------------
     (   n : Nat   !                                                          
data !-------------!                                                          
     ! DataP n : * )                                                          
                                                                              
where (--------------------!                                                  
      ! dz : DataP (suc n) )                                                  
                                                                              
      (     a : DataP n      !                                                
      !----------------------!                                                
      ! ds a : DataP (suc n) )                                                
                                                                              
      ( a : DataP n ;  b : DataP (suc n) !                                    
      !----------------------------------!                                    
      !        dlet a b : DataP n        )                                    
                                                                              
      (-----------------!                                                     
      ! dzero : DataP n )                                                     
                                                                              
      ( a, b :     !                     ( a, b :     !    ( a :             !
      !   DataP n  !                     !   DataP n  !    !   DataP (suc n) !
      !------------! ;  (-----------! ;  !------------! ;  !-----------------!
      ! dplus a b  !    ! done :    !    ! dtimes a b !    ! mu a : DataP n  )
      !  : DataP n )    !   DataP n )    !  : DataP n )                       
------------------------------------------------------------------------------
     (  n : Nat  !                               ( as : Tel n ;  a : DataP n !
data !-----------!  where (-----------------! ;  !---------------------------!
     ! Tel n : * )        ! temp : Tel zero )    !  text as a : Tel (suc n)  )
------------------------------------------------------------------------------
     ( as : Tel n ;  a : DataP n !                                          
data !---------------------------!                                          
     !       ValT as a : *       )                                          
                                                                            
      (       x : ValT as a        !                                        
where !----------------------------!                                        
      ! vz x : ValT (text as a) dz )                                        
                                                                            
      ( as : Tel n ;  x : ValT as a ;  b : DataP n !                        
      !--------------------------------------------!                        
      !       vs x : ValT (text as b) (ds a)       )                        
                                                                            
      (   x : ValT (text as a) b    !                                       
      !-----------------------------!                                       
      ! vlet x : ValT as (dlet a b) )                                       
                                                                            
      ( as : Tel n ;  x : ValT as a ;  b : DataP n !                        
      !--------------------------------------------!                        
      !        inl x : ValT as (dplus a b)         )                        
                                                                            
      ( as : Tel n ;  x : ValT as b ;  a : DataP n !                        
      !--------------------------------------------!                        
      !        inr x : ValT as (dplus a b)         )                        
                                                                            
      (---------------------!                                               
      ! void : ValT as done )                                               
                                                                            
      ( x : ValT as a ;  y : ValT as b  !    ( x : ValT (text as (mu f)) f !
      !---------------------------------! ;  !-----------------------------!
      ! pair x y : ValT as (dtimes a b) )    !    in x : ValT as (mu f)    )
------------------------------------------------------------------------------
let  (----------!      
     ! Data : * )      
                       
     Data => DataP zero
------------------------------------------------------------------------------
     ( d : Data  !       
let  !-----------!       
     ! Val d : * )       
                         
     Val d => ValT temp d
------------------------------------------------------------------------------
let  (------------!           
     ! nat : Data )           
                              
     nat => mu (dplus done dz)
------------------------------------------------------------------------------
let  (--------------!   
     ! nz : Val nat )   
                        
     nz => in (inl void)
------------------------------------------------------------------------------
     (   n : Val nat    !   
let  !------------------!   
     ! ns n : (Val nat) )   
                            
     ns n => in (inr (vz n))
------------------------------------------------------------------------------
data (----------!  where true : Bool ;  false : Bool
     ! Bool : * )                                   
------------------------------------------------------------------------------
     (  b, c : Bool   !    
let  !----------------!    
     ! and b c : Bool )    
                           
     and b c <= case b     
     { and true c => c     
       and false c => false
     }                     
------------------------------------------------------------------------------
     ( x, y : ValT as a !                                       
let  !------------------!                                       
     !  eq x y : Bool   )                                       
                                                                
     eq x y <= rec x                                            
     { eq x y <= case x                                         
       { eq (vz x) y <= case y                                  
         { eq (vz x') (vz x) => eq x' x                         
         }                                                      
         eq (vs x) y <= case y                                  
         { eq (vs x') (vs x) => eq x' x                         
         }                                                      
         eq (vlet x) y <= case y                                
         { eq (vlet x') (vlet x) => eq x' x                     
         }                                                      
         eq (inl x) y <= case y                                 
         { eq (inl x') (inl x) => eq x' x                       
           eq (inl x') (inr x) => false                         
         }                                                      
         eq (inr x) y <= case y                                 
         { eq (inr x') (inl x) => false                         
           eq (inr x') (inr x) => eq x' x                       
         }                                                      
         eq void y <= case y                                    
         { eq void void => true                                 
         }                                                      
         eq (pair x y) y' <= case y'                            
         { eq (pair x' y') (pair x y) => and (eq x' x) (eq y' y)
         }                                                      
         eq (in x) y <= case y                                  
         { eq (in x') (in x) => eq x' x                         
         }                                                      
       }                                                        
     }                                                          
------------------------------------------------------------------------------
inspect [eq nz nz] => ? : ?
------------------------------------------------------------------------------
inspect [eq (ns nz) nz] => ? : ?
------------------------------------------------------------------------------
inspect [eq (ns nz) (ns nz)] => ? : ?
------------------------------------------------------------------------------