---------------------------------------------------------------------------------------
     (  A, B : *   !        (   a : A ;  b : B   !
data !-------------!  where !--------------------!
     ! And A B : * )        ! pair a b : And A B )
---------------------------------------------------------------------------------------
     (  A, B : *  !        (      a : A      !    (      b : B       !
data !------------!  where !-----------------! ;  !------------------!
     ! Or A B : * )        ! left a : Or A B )    ! right b : Or A B )
---------------------------------------------------------------------------------------
     (   A : *   !     
let  !-----------!     
     ! Not A : * )     
                       
     Not A => A -> Zero
---------------------------------------------------------------------------------------
     ( P : A -> * !        ( a : A ;  p : P a !
data !------------!  where !------------------!
     !  Ex P : *  )        !  wit a p : Ex P  )
---------------------------------------------------------------------------------------
     ( P, Q : A -> * ;  p : Ex (lam a => Or (P a) (Q a)) !
let  !---------------------------------------------------!
     !           exorlem p : Or (Ex P) (Ex Q)            )
                                                          
     exorlem p <= case p                                  
     { exorlem (wit a p) <= case p                        
       { exorlem (wit a (left a')) => left (wit a a')     
         exorlem (wit a (right b)) => right (wit a b)     
       }                                                  
     }                                                    
---------------------------------------------------------------------------------------
     (  P, Q : A -> * ;  p : Or (Ex P) (Ex Q)   !    
let  !------------------------------------------!    
     ! orexlem p : Ex (lam a => Or (P a) (Q a)) )    
                                                     
     orexlem p <= case p                             
     { orexlem (left a) <= case a                    
       { orexlem (left (wit a p)) => wit a (left p)  
       }                                             
       orexlem (right b) <= case b                   
       { orexlem (right (wit a p)) => wit a (right p)
       }                                             
     }                                               
---------------------------------------------------------------------------------------
data (----------!  where (-------------! ;  (--------------!
     ! Bool : * )        ! true : Bool )    ! false : Bool )
---------------------------------------------------------------------------------------
     (   b : Bool   !   
let  !--------------!   
     ! not b : Bool )   
                        
     not b <= case b    
     { not true => false
       not false => true
     }                  
---------------------------------------------------------------------------------------
     (           b : Bool            !
let  !-------------------------------!
     ! notnotLem b : not (not b) = b )
                                      
     notnotLem b <= case b            
     { notnotLem true => refl         
       notnotLem false => refl        
     }                                
---------------------------------------------------------------------------------------
     (  b, c : Bool   !         
let  !----------------!         
     ! eqb b c : Bool )         
                                
     eqb b c <= case b          
     { eqb true c <= case c     
       { eqb true true => true  
         eqb true false => false
       }                        
       eqb false c <= case c    
       { eqb false true => false
         eqb false false => true
       }                        
     }                          
---------------------------------------------------------------------------------------
inspect eqb false true => false : Bool
---------------------------------------------------------------------------------------
     ( p : true = false !
let  !------------------!
     !  tnef p : Zero   )
                         
     tnef p <= case p    
---------------------------------------------------------------------------------------
     ( a, b : A ;  p : a = b !
let  !-----------------------!
     !     sym p : b = a     )
                              
     sym p <= case p          
     { sym refl => refl       
     }                        
---------------------------------------------------------------------------------------
     (             b, c : Bool             !             
let  !-------------------------------------!             
     ! eqbb b c : Or (b = c) (Not (b = c)) )             
                                                         
     eqbb b c <= case b                                  
     { eqbb true c <= case c                             
       { eqbb true true => left refl                     
         eqbb true false => right tnef                   
       }                                                 
       eqbb false c <= case c                            
       { eqbb false true => right (lam x => tnef (sym x))
         eqbb false false => left refl                   
       }                                                 
     }                                                   
---------------------------------------------------------------------------------------
inspect eqbb false true                                     
          =>                                                
          right (lam x => tnef (sym x)) :                   
            Or (false = true) (all x : false = true => Zero)
---------------------------------------------------------------------------------------
inspect eqbb true true => left refl : Or (true = true) (all x : true = true => Zero)
---------------------------------------------------------------------------------------
                                          (   n : Nat   !
data (---------!  where (------------! ;  !-------------!
     ! Nat : * )        ! zero : Nat )    ! suc n : Nat )
---------------------------------------------------------------------------------------
let  (-----------!  
     ! one : Nat )  
                    
     one => suc zero
---------------------------------------------------------------------------------------
let  (-----------! 
     ! two : Nat ) 
                   
     two => suc one
---------------------------------------------------------------------------------------
let  (-------------! 
     ! three : Nat ) 
                     
     three => suc two
---------------------------------------------------------------------------------------
     (  m, n : Nat   !               
let  !---------------!               
     ! add m n : Nat )               
                                     
     add m n <= case m               
     { add zero n => n               
       add (suc m) n => suc (add m n)
     }                               
---------------------------------------------------------------------------------------
inspect add two two => ? : Nat
---------------------------------------------------------------------------------------
inspect add zero two => suc (suc zero) : Nat
---------------------------------------------------------------------------------------
let  (---------------! ;  absurd => absurd
     ! absurd : Zero )                    
---------------------------------------------------------------------------------------
     (   m, n : Nat   !                  
let  !----------------!                  
     ! add' m n : Nat )                  
                                         
     add' m n <= rec m                   
     { add' m n <= case m                
       { add' zero n => n                
         add' (suc m) n => suc (add' m n)
       }                                 
     }                                   
---------------------------------------------------------------------------------------
inspect add' two two => suc (suc (suc (suc zero))) : Nat
---------------------------------------------------------------------------------------