---------------------------------------------------------------------------------------
[]
---------------------------------------------------------------------------------------
     (  A, B : *  !        (      a : A      !    (      b : B       !
data !------------!  where !-----------------! ;  !------------------!
     ! Or A B : * )        ! left a : Or A B )    ! right b : Or A B )
---------------------------------------------------------------------------------------
     (  A, B : *   !        (   a : A ;  b : B   !
data !-------------!  where !--------------------!
     ! And A B : * )        ! pair a b : And A B )
---------------------------------------------------------------------------------------
     (   A : *   !     
let  !-----------!     
     ! Not A : * )     
                       
     Not A => A -> 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 <= rec m                  
     { add m n <= case m               
       { add zero n => n               
         add (suc m) n => suc (add m n)
       }                               
     }                                 
---------------------------------------------------------------------------------------
     ( a, b : A ;  p : a = b !
let  !-----------------------!
     !    eqSym p : b = a    )
                              
     eqSym p <= case p        
     { eqSym refl => refl     
     }                        
---------------------------------------------------------------------------------------
     ( a, b, c : A ;  p : a = b ;  q : b = c !
let  !---------------------------------------!
     !          eqTrans p q : a = c          )
                                              
     eqTrans p q <= case p                    
     { eqTrans refl q => q                    
     }                                        
---------------------------------------------------------------------------------------
     (  f : A -> B ;  p : a = b   !
let  !----------------------------!
     ! eqResp f p : (f a) = (f b) )
                                   
     eqResp f p <= case p          
     { eqResp f refl => refl       
     }                             
---------------------------------------------------------------------------------------
     ( f : A -> B -> C ;  p : a = b ;  q : c = d !
let  !-------------------------------------------!
     !       eqResp2 f p q : f a c = f b d       )
                                                  
     eqResp2 f p q <= case p                      
     { eqResp2 f refl q <= case q                 
       { eqResp2 f refl refl => refl              
       }                                          
     }                                            
---------------------------------------------------------------------------------------
     ( P : A -> * ;  a, b : A ;  q : a = b ;  p : P a !
let  !------------------------------------------------!
     !               eqSubst q p : P b                )
                                                       
     eqSubst q p <= case q                             
     { eqSubst refl p => p                             
     }                                                 
---------------------------------------------------------------------------------------
     (   P : *   !        
let  !-----------!        
     ! Dec P : * )        
                          
     Dec P => Or P (Not P)
---------------------------------------------------------------------------------------
     ( p : zero = suc n !
let  !------------------!
     !  znes p : Empty  )
                         
     znes p <= case p    
---------------------------------------------------------------------------------------
     ( p : suc m = suc n !
let  !-------------------!
     ! injSuc p : m = n  )
                          
     injSuc p <= case p   
     { injSuc refl => refl
     }                    
---------------------------------------------------------------------------------------
     (          p : Dec (m = n)          !             
let  !-----------------------------------!             
     ! eqSuc p : Dec ((suc m) = (suc n)) )             
                                                       
     eqSuc p <= case p                                 
     { eqSuc (left refl) => left refl                  
       eqSuc (right b) => right (lam p => b (injSuc p))
     }                                                 
---------------------------------------------------------------------------------------
     (      m, n : Nat       !                                
let  !-----------------------!                                
     ! eq' m n : Dec (m = n) )                                
                                                              
     eq' m n <= rec m                                         
     { eq' m n <= case m                                      
       { eq' zero n <= case n                                 
         { eq' zero zero => left refl                         
           eq' zero (suc n) => right (lam p => znes p)        
         }                                                    
         eq' (suc m) n <= case n                              
         { eq' (suc m) zero => right (lam p => znes (eqSym p))
           eq' (suc m) (suc n) => eqSuc (eq' m n)             
         }                                                    
       }                                                      
     }                                                        
---------------------------------------------------------------------------------------
inspect eq' one two                                                                   
          =>                                                                          
          right (lam p => znes (injSuc p)) :                                          
            Or (suc zero = suc (suc zero)) (all x : suc zero = suc (suc zero) => Zero)
---------------------------------------------------------------------------------------
inspect eq' two two                                            
          =>                                                   
          left refl :                                          
            Or (suc (suc zero) = suc (suc zero))               
            % (all x : suc (suc zero) = suc (suc zero) => Zero)
---------------------------------------------------------------------------------------
     (   A : *    !                            ( a : A ;  as : List A !
data !------------!  where (--------------! ;  !----------------------!
     ! List A : * )        ! nil : List A )    !  cons a as : List A  )
---------------------------------------------------------------------------------------
let  (-----------------!                         
     ! l123 : List Nat )                         
                                                 
     l123 => cons one (cons two (cons three nil))
---------------------------------------------------------------------------------------
     (  as : List A   !                     
let  !----------------!                     
     ! count as : Nat )                     
                                            
     count as <= rec as                     
     { count as <= case as                  
       { count nil => zero                  
         count (cons a as) => suc (count as)
       }                                    
     }                                      
---------------------------------------------------------------------------------------
inspect count l123 => suc (suc (suc zero)) : Nat
---------------------------------------------------------------------------------------
     (    as, bs : List A    !                         
let  !-----------------------!                         
     ! append as bs : List A )                         
                                                       
     append as bs <= rec as                            
     { append as bs <= case as                         
       { append nil bs => bs                           
         append (cons a as) bs => cons a (append as bs)
       }                                               
     }                                                 
---------------------------------------------------------------------------------------
inspect append l123 l123                                                              
          =>                                                                          
          cons (suc zero) (cons (suc (suc zero))                          ! : List Nat
                          !% (cons (suc (suc (suc zero)))                !!           
                          !  !% (cons (suc zero)                        !!!           
                          !  !  !% (cons (suc (suc zero))              !!!!           
                          !  !  !  !% (cons (suc (suc (suc zero))) nil)))))           
---------------------------------------------------------------------------------------
     (   as : List A   !                                
let  !-----------------!                                
     ! rev as : List A )                                
                                                        
     rev as <= rec as                                   
     { rev as <= case as                                
       { rev nil => nil                                 
         rev (cons a as) => append (rev as) (cons a nil)
       }                                                
     }                                                  
---------------------------------------------------------------------------------------
inspect rev l123                                                                   
          =>                                                                       
          cons (suc (suc (suc zero))) (cons (suc (suc zero)) (cons (suc zero) nil))
           : List Nat                                                              
---------------------------------------------------------------------------------------
     (               a : A ;  as : List A               !                     
let  !--------------------------------------------------! ;  revlemlem a as []
     ! revlemlem a as :                                 !                     
     !   rev (append as (cons a nil)) = cons a (rev as) )                     
---------------------------------------------------------------------------------------
     (          as : List A          !                                    
let  !-------------------------------!                                    
     ! revLem as : rev (rev as) = as )                                    
                                                                          
     revLem as <= rec as                                                  
     { revLem as <= case as                                               
       { revLem nil => refl                                               
         revLem (cons a as)                                               
           => eqTrans (revlemlem a (rev as)) (eqResp (cons a) (revLem as))
       }                                                                  
     }                                                                    
---------------------------------------------------------------------------------------