------------------------------------------------------------------------------
                                      (   n : Nat    !
data (---------!  where zero : Nat ;  !--------------!
     ! Nat : * )                      ! succ n : Nat )
------------------------------------------------------------------------------
     (   m, n : Nat   !                    
let  !----------------!                    
     ! plus m n : Nat )                    
                                           
     plus m n <= rec m                     
     { plus m n <= case m                  
       { plus zero n => n                  
         plus (succ m) n => succ (plus m n)
       }                                   
     }                                     
------------------------------------------------------------------------------
     (  n : Nat  !                                 (      i : Fin n      !
data !-----------!  where (-------------------! ;  !---------------------!
     ! Fin n : * )        ! fz : Fin (succ n) )    ! fs i : Fin (succ n) )
------------------------------------------------------------------------------
     ( j : Fin zero ! 
let  !--------------! 
     ! magic j : A  ) 
                      
     magic j <= case j
------------------------------------------------------------------------------
     (    i : Fin b    !                   
let  !-----------------!                   
     ! project i : Nat )                   
                                           
     project i <= rec i                    
     { project i <= case i                 
       { project fz => zero                
         project (fs i) => succ (project i)
       }                                   
     }                                     
------------------------------------------------------------------------------
     ( b, n : Nat !        (    i : Fin b    !                      
data !------------!  where !-----------------! ;  (----------------!
     !  Bounded   !        ! inBound i :     !    ! outBound b k : !
     !  % b n     !        !   Bounded b     !    !   Bounded b    !
     !   : *      )        !   % (project i) )    !   % (plus b k) )
------------------------------------------------------------------------------
let  (---------------------------!                                    
     ! bounded b n : Bounded b n )                                    
                                                                      
     bounded b n <= rec b                                             
     { bounded b n <= case b                                          
       { bounded zero n => outBound zero n                            
         bounded (succ b) n <= case n                                 
         { bounded (succ b) zero => inBound fz                        
           bounded (succ b) (succ n) <= view bounded b n              
           { bounded (succ b) (succ (project i)) => inBound (fs i)    
             bounded (succ b) (succ (plus b k)) => outBound (succ b) k
           }                                                          
         }                                                            
       }                                                              
     }                                                                
------------------------------------------------------------------------------
inspect bounded (succ zero) zero => inBound fz : Bounded (succ zero) zero
------------------------------------------------------------------------------
inspect bounded (succ (succ (succ zero)))                      
        % (succ (succ (succ (succ (succ (zero))))))            
          =>                                                   
          outBound (succ (succ (succ zero))) (succ (succ zero))
           : Bounded (succ (succ (succ zero)))                 
             % (succ (succ (succ (succ (succ zero)))))         
------------------------------------------------------------------------------