----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( a, b : A ;  q : a = b ;  P : all x : A => * ;  p : P a !
let  !--------------------------------------------------------!
     !                  substL2R q P p : P b                  )
                                                               
     substL2R q P p <= case q                                  
     { substL2R refl P p => p                                  
     }                                                         
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( x, y : T ;  f : T -> U ;  q : x = y ;  P : U -> * ;  p : P (f x) !
let  !------------------------------------------------------------------!
     !                      resp f q P p : P (f y)                      )
                                                                         
     resp f q P p <= case q                                              
     { resp f refl P p => p                                              
     }                                                                   
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
data (----------!  where (-----------! ;  (-----------!
     ! Bool : * )        ! tt : Bool )    ! ff : Bool )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( b : Bool ;  e1, e2 : T !
let  !------------------------!
     !    cond b e1 e2 : T    )
                               
     cond b e1 e2 <= case b    
     { cond tt e1 e2 => e1     
       cond ff e1 e2 => e2     
     }                         
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
                                          (   n : Nat    !
data (---------!  where (------------! ;  !--------------!
     ! Nat : * )        ! zero : Nat )    ! succ n : Nat )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     (   x, y : Nat   !                    
let  !----------------!                    
     ! plus x y : Nat )                    
                                           
     plus x y <= rec x                     
     { plus x y <= case x                  
       { plus zero y => y                  
         plus (succ n) y => succ (plus n y)
       }                                   
     }                                     
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
data (----------!  where (------------! ;  (-------------!
     ! TExp : * )        ! nat : TExp )    ! bool : TExp )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( T : TExp  !     
let  !-----------!     
     ! Val T : * )     
                       
     Val T <= case T   
     { Val nat => Nat  
       Val bool => Bool
     }                 
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( T : TExp  !        (    v : Val T    !    (  e1, e2 : Exp nat   !    ( b : Exp bool ;  e1, e2 : Exp T !
data !-----------!  where !-----------------! ;  !---------------------! ;  !--------------------------------!
     ! Exp T : * )        ! val T v : Exp T )    ! add e1 e2 : Exp nat )    !       if b e1 e2 : Exp T       )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     (   e : Exp T    !                                        
let  !----------------!                                        
     ! eval e : Val T )                                        
                                                               
     eval e <= rec e                                           
     { eval x <= case x                                        
       { eval (val T v) => v                                   
         eval (add e1 e2) => plus (eval e1) (eval e2)          
         eval (if b e1 e2) => cond (eval b) (eval e1) (eval e2)
       }                                                       
     }                                                         
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     (   A : *    !                            ( a : A ;  as : List A !
data !------------!  where (--------------! ;  !----------------------!
     ! List A : * )        ! nil : List A )    !  cons a as : List A  )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
let  (---------------!     
     ! StackType : * )     
                           
     StackType => List TExp
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( S : StackType !                                (   val : Val T ;  stack : TyStack S    !
data !---------------!  where StackE : TyStack nil ;  !---------------------------------------!
     ! TyStack S : * )                                ! push T val stack : TyStack (cons T S) )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( S, S' : StackType !                        ( c1 : Code S1 S2 ;  c2 : Code S2 S3 !    (   v : Val T    !                                          (  c1, c2 : Code S1 S2  !
data !-------------------!  where (----------! ;  !------------------------------------! ;  !----------------! ;  (--------------------------------! ;  !-----------------------!
     !   Code S S' : *   )        ! skip :   !    !       seq c1 c2 : Code S1 S3       )    ! PUSH T v :     !    ! ADD :                          !    ! IF c1 c2 :            !
                                  !   Code S !                                              !   Code S       !    !   Code (cons nat (cons nat S)) !    !   Code (cons bool! S2 !
                                  !   % S    )                                              !   % (cons T S) )    !   % (cons nat S)               )    !        !% S1     )    )
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( code : Code S T ;  s : TyStack S !                                   
let  !----------------------------------!                                   
     !     exec code s : TyStack T      )                                   
                                                                            
     exec code s <= rec code                                                
     { exec c s <= case c                                                   
       { exec skip s => s                                                   
         exec (seq c1 c2) s => exec c2 (exec c1 s)                          
         exec (PUSH T v) s => push T v s                                    
         exec ADD s <= case s                                               
         { exec ADD (push nat m s) <= case s                                
           { exec ADD (push nat n (push nat m s)) => push nat (plus n m) s  
           }                                                                
         }                                                                  
         exec (IF c1 c2) s <= case s                                        
         { exec (IF c1 c2) (push bool v s) => cond v (exec c1 s) (exec c2 s)
         }                                                                  
       }                                                                    
     }                                                                      
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     (   S : StackType ;  e : Exp T    !                                               
let  !---------------------------------!                                               
     ! compile S e : Code S (cons T S) )                                               
                                                                                       
     compile S e <= rec e                                                              
     { compile S x <= case x                                                           
       { compile S (val T v) => PUSH T v                                               
         compile S (add e1 e2) => seq (compile ? e2) (seq (compile ? e1) ADD)          
         compile S (if b e1 e2) => seq (compile ? b) (IF (compile ? e1) (compile ? e2))
       }                                                                               
     }                                                                                 
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( e1, e2 : Exp nat                                                                                                                                                             !
     !                                                                                                                                                                              !
     ! s : TyStack S ;  c1 : push nat (eval e1) (push nat (eval e2) s) = exec (compile (cons nat S) e1) (push nat (eval e2) s) ;  c2 : push nat (eval e2) s = exec (compile S e2) s !
let  !------------------------------------------------------------------------------------------------------------------------------------------------------------------------------!
     !                                     correctAdd e1 e2 S s c1 c2 : push nat (plus (eval e1) (eval e2)) s = exec (compile S (add e1 e2)) s                                      )
                                                                                                                                                                                     
     correctAdd e1 e2 S s c1 c2                                                                                                                                                      
       =>                                                                                                                                                                            
       substL2R c2 (lam x => (push nat (plus (eval e1) (eval e2)) s) = (exec ADD (exec (compile (cons nat S) e1) x)))                                                                
       % (substL2R c1 (lam y => (push nat (plus (eval e1) (eval e2)) s) = exec ADD y) refl)                                                                                          
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     ( e1, e2 : Exp T ;  s : TyStack S ;  c1 : push T (eval e1) s = exec (compile S e1) s ;  c2 : push T (eval e2) s = exec (compile S e2) s ;  b : Bool !
let  !---------------------------------------------------------------------------------------------------------------------------------------------------!
     !          correctIf T e1 e2 S s c1 c2 b : push T (cond b (eval e1) (eval e2)) s = cond b (exec (compile S e1) s) (exec (compile S e2) s)           )
                                                                                                                                                          
     correctIf T e1 e2 S s c1 c2 b <= case b                                                                                                              
     { correctIf T e1 e2 S s c1 c2 tt => c1                                                                                                               
       correctIf T e1 e2 S s c1 c2 ff => c2                                                                                                               
     }                                                                                                                                                    
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
     (                e : Exp T ;  s : TyStack S                !                                                                         
let  !----------------------------------------------------------!                                                                         
     ! correct T e s : push T (eval e) s = exec (compile S e) s )                                                                         
                                                                                                                                          
     correct T e s <= rec e                                                                                                               
     { correct T x s <= case x                                                                                                            
       { correct T (val T v) s => refl                                                                                                    
         correct nat (add e1 e2) s => correctAdd e1 e2 ? s (correct nat e1 (push ? (eval e2) s)) (correct nat e2 s)                       
         correct T (if b e1 e2) s                                                                                                         
           =>                                                                                                                             
           substL2R (correct bool b s) (lam x => push T (cond (eval b) (eval e1) (eval e2)) s = exec (IF (compile ? e1) (compile ? e2)) x)
           % (correctIf ? e1 e2 ? s (correct T e1 s) (correct T e2 s) (eval b))                                                           
       }                                                                                                                                  
     }                                                                                                                                    
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------