---------------------------------------------------------------------------------------
     (  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 : And A B !      
let  !-------------!      
     !  fst p : A  )      
                          
     fst p <= case p      
     { fst (pair a b) => a
     }                    
---------------------------------------------------------------------------------------
     ( p : And A B !      
let  !-------------!      
     !  snd p : B  )      
                          
     snd p <= case p      
     { snd (pair a b) => b
     }                    
---------------------------------------------------------------------------------------
     ( X : * ;  P, Q : X -> * ;  p : all x : X => And (P x) (Q x) !
let  !------------------------------------------------------------!
     !  allAndLem p : And (all x : X => P x) (all x : X => Q x)   )
                                                                   
     allAndLem p => pair (lam x => fst (p x)) (lam x => snd (p x)) 
---------------------------------------------------------------------------------------
     (                            X : * ;  P, Q : X -> *                             !
let  !-------------------------------------------------------------------------------!
     ! allAndLem' :                                                                  !
     !   (all x : X => And (P x) (Q x)) -> And (all x : X => P x) (all x : X => Q x) )
                                                                                      
     allAndLem' => allAndLem                                                          
---------------------------------------------------------------------------------------
     ( X : * ;  P, Q : X -> * ;  q : And (all x : X => P x) (all x : X => Q x) !
let  !-------------------------------------------------------------------------!
     !               andAllLem q : all x : X => And (P x) (Q x)                )
                                                                                
     andAllLem q <= case q                                                      
     { andAllLem (pair a b) => lam x => pair (a x) (b x)                        
     }                                                                          
---------------------------------------------------------------------------------------
data (----------!  where (-------------! ;  (--------------!
     ! Bool : * )        ! true : Bool )    ! false : Bool )
---------------------------------------------------------------------------------------
     (   b : Bool   !   
let  !--------------!   
     ! not b : Bool )   
                        
     not b <= case b    
     { not true => false
       not false => true
     }                  
---------------------------------------------------------------------------------------
inspect not true => false : Bool
---------------------------------------------------------------------------------------
inspect not (not true) => true : Bool
---------------------------------------------------------------------------------------
     ( A : * ;  a, b : A !                          
data !-------------------!  where (----------------!
     !    Eq a b : *     )        ! refl' : Eq a a )
---------------------------------------------------------------------------------------
     (             b : Bool             !
let  !----------------------------------!
     ! notnotLem b : Eq (not (not b)) b )
                                         
     notnotLem b <= case b               
     { notnotLem true => refl'           
       notnotLem false => refl'          
     }                                   
---------------------------------------------------------------------------------------
     ( A : * ;  a, b : A ;  p : Eq a b !
let  !---------------------------------!
     !         sym p : Eq b a          )
                                        
     sym p <= case p                    
     { sym refl' => refl'               
     }                                  
---------------------------------------------------------------------------------------
     ( p : Eq a b ;  q : Eq b c !
let  !--------------------------!
     !    trans p q : Eq a c    )
                                 
     trans p q <= case p         
     { trans refl' q => q        
     }                           
---------------------------------------------------------------------------------------
     ( p : true = false !
let  !------------------!
     !  tnef p : Zero   )
                         
     tnef p <= case p    
---------------------------------------------------------------------------------------
     ( f : A -> B ;  p : a = b !
let  !-------------------------!
     !  resp f p : f a = f b   )
                                
     resp f p <= case p         
     { resp f refl => refl      
     }                          
---------------------------------------------------------------------------------------
     ( f : A -> B ;  p : f a = f b !
let  !-----------------------------!
     !     garbage f p : a = b     )
                                    
     garbage f p <= case p          
     { garbage f p []               
     }                              
---------------------------------------------------------------------------------------