------------------------------------------------------------------------------
                                      (   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]
       }                                       
     }                                         
------------------------------------------------------------------------------