---------------------------------------------------------------------------------------
     (  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 )
---------------------------------------------------------------------------------------
     (        p : (And (Or A B) C)         !              
let  !-------------------------------------!              
     ! andorlem p : Or (And A C) (And B C) )              
                                                          
     andorlem p <= case p                                 
     { andorlem (pair a b) <= case a                      
       { andorlem (pair (left a) b) => left (pair a b)    
         andorlem (pair (right b) b') => right (pair b b')
       }                                                  
     }                                                    
---------------------------------------------------------------------------------------
let  (------------------------------------------------------!
     ! andorlem' : And (Or A B) C -> Or (And A C) (And B C) )
                                                             
     andorlem' => lam g => andorlem g                        
---------------------------------------------------------------------------------------
     (    p : And A B     !         
let  !--------------------!         
     ! andcom p : And B A )         
                                    
     andcom p <= case p             
     { andcom (pair a b) => pair b a
     }                              
---------------------------------------------------------------------------------------
     (    p : Or A B    !       
let  !------------------!       
     ! orcom p : Or B A )       
                                
     orcom p <= case p          
     { orcom (left a) => right a
       orcom (right b) => left b
     }                          
---------------------------------------------------------------------------------------
data (-----------!  where 
     ! False : * )        
---------------------------------------------------------------------------------------
     ( p : False ;  A : * !
let  !--------------------!
     !     efq p : A      )
                           
     efq p <= case p       
---------------------------------------------------------------------------------------