%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Lemma 17 : Data-stack substitution
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

www : vvalMS XXi Xi -> vvalT XXi T XXi' -> dstack_substT T Xi T' Xi'
      -> vvalMS XXi' Xi' -> type.

www_vstack_v : {v:ctriv}
               {vvv:{xi:stack}vvalT (xi , v) v xi}
               {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
               www (vvalMS_v VVMS) (vvv XXi) (dsv Xi v) VVMS.

www_tstack_v : {v:ctriv}
               {vvv:{xi:stack}vvalT (xi , v) v xi}
               {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
               www (vvalMS_t VVMS VVT) (vvv XXi) (dsv Xi T) VVMS.

www_stack_t : {t:ctriv}
              {vvt:{xi:stack}vvalT xi t xi}
              {dst:{xi:stack}dstack_substT t xi t xi}
              www VVMS (vvt XXi) (dst Xi) VVMS.


lappT : dstack_substT T Xi T' Xi' 
        -> app (Xi1 & Xi) NXi -> app (Xi1 & Xi') NXi'
        -> dstack_substT T NXi T' NXi' -> type. 
               
lappT_v : {v:ctriv}
          {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
          lappT (dsv Xi T) (app_stack APP) APP (dsv Xi1 T).


lappT_t : {t:ctriv}
          {dst:{xi:stack}dstack_substT t xi t xi}
          lappT (dst Xi) APP APP (dst Xi1).

lemma17-1E : vvalE XXi E -> dstack_substE E XXi E -> type.


lemma17-1T : vvalT XXi T XXi' -> dstack_substT T XXi T XXi' 
             -> type.

lemma17-1C : vvalC XXi C -> dstack_substC C XXi C -> type.


lemma17-1_t : {t:ctriv}
              {vvt:{xi:stack}vvalT xi t xi}
              {dst:{xi:stack}dstack_substT t xi t xi}
              lemma17-1T (vvt XXi) 
                         (dst XXi).

lemma17-1_v : {v:ctriv}
              {vvv:{xi:stack}vvalT (xi , v) v xi}
              {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
              lemma17-1T (vvv XXi) 
                         (dsv XXi v).

lemma17-1_cret : lemma17-1E (vval_cret VVC VVT) 
                            (dstack_subst_cret DSC DST)
                 <- lemma17-1T VVT DST
                 <- lemma17-1C VVC DSC.

lemma17-1_capp : lemma17-1E (vval_capp VVC VVT0 VVT1) 
                            (dstack_subst_capp DSC DST0 DST1)
                 <- lemma17-1T VVT0 DST0
                 <- lemma17-1T VVT1 DST1
                 <- lemma17-1C VVC DSC.


lemma17-1_vlam : lemma17-1C (vval_vlam VE)
                            (dstack_subst_vlam DE)
               <- {v:ctriv}
                  {vvv:{xi:stack}vvalT (xi , v) v xi}
                  {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                  lemma17-1E (VE v vvv) (DE v dsv).

lemma17-2 : {t:ctriv -> ctriv}
            ({v:ctriv}app ((XXi , v) & XXi') (XXi1 v))
            -> ({v:ctriv}{vvv:{xi:stack}vvalT (xi , v) v xi}
                vvalE (XXi1 v) (E v))
            -> ({v:ctriv}app ((Xi , v) & Xi') (Xi1 v))
            -> ({v:ctriv}vvalMS (XXi1 v) (Xi1 (t v)))
            -> ({v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                dstack_substE (E v) (Xi1 v) (E' v))
            -> ({v:ctriv}{dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                dstack_substE (E v) (Xi1 (t v)) (E' (t v)))
            -> type.   

lemma17-3 : ({k:ccont}{vvk:vvalC dot k}vvalE XXi (E k)) 
            -> cvalE E 
            -> vvalC XXi' C
            -> vvalMS XXi Xi
            -> vvalDS XXi' Xi'
            -> app (Xi' & Xi) Xi0
            -> dstack_substC C Xi' C'
            -> dstack_substE (E C') Xi E1
            -> dstack_substE (E C) Xi0 E1  
            -> type.



lemma17-2_cret_v1 : ({v1:ctriv}
                     {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi}
                     {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                     lemma17-2 T
                               ([v:ctriv]app_stack (APP v))
                               ([v:ctriv][vvv]
                                 vval_cret (vval_vlam [v2:ctriv][vvv2]
                                                       VVE v2 vvv2 v vvv) 
                                           (vvv1 (XXi v)))
                               ([v:ctriv]app_stack (APP1 v))
                               (VVMS v1)
                               ([v:ctriv][dsv]
                                 dstack_subst_cret 
                                    (dstack_subst_vlam [v2:ctriv][dsv2]
                                                        (DSE v2 dsv2 v dsv))
                                    (dsv1 (Xi v) (T1 v1)))
                               ([v:ctriv][dsv]
                                 dstack_subst_cret 
                                    (dstack_subst_vlam [v2:ctriv][dsv2]
                                                        (DSE' v2 dsv2 v dsv))
                                    (dsv1 (Xi (T v)) (T1 v1))))
                    <- ({v:ctriv}{v1:ctriv}
                        {dsv1:{xi:stack}{t:ctriv}
                              dstack_substT v1 (xi , t) t xi}
                        {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                        www (VVMS v1 v) (vvv1 (XXi v)) 
                            (dsv1 (Xi (T v)) (T1 v1)) (VVMS' v))
                    <- {v2:ctriv}
                       {dsv2:{xi:stack}{t:ctriv}dstack_substT v2 (xi , t) t xi}
                       {vvv2:{xi:stack}vvalT (xi , v2) v2 xi}
                       lemma17-2 T
                                 ([v:ctriv]app_stack (APP v))
                                 (VVE' v2 vvv2)
                                 ([v:ctriv]app_stack (APP1 v))
                                 ([v:ctriv]vvalMS_v (VVMS' v)) 
                                 (DSE v2 dsv2)
                                 (DSE' v2 dsv2).
               

lemma17-2_cret_t : ({t:ctriv}
                    {dst:{xi:stack}dstack_substT t xi t xi}
                    {vvt:{xi:stack}vvalT xi t xi}
                    lemma17-2 T'
                              APP
                              ([v:ctriv][vvv]
                                vval_cret (vval_vlam [v1:ctriv][vvv1]
                                                      (VVE v1 vvv1 v vvv))
                                          (vvt (XXi v)))
                              APP1
                              VVMS
                              ([v:ctriv][dsv]
                                dstack_subst_cret 
                                 (dstack_subst_vlam [v1:ctriv][dsv1]
                                                     (DSE v1 dsv1 v dsv))
                                 (dst (Xi , v)))
                              ([v:ctriv][dsv]
                                dstack_subst_cret 
                                 (dstack_subst_vlam [v1:ctriv][dsv1]
                                                     (DSE' v1 dsv1 v dsv))
                                 (dst (Xi , (T' v)))))
                    <- {v1:ctriv}
                       {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi}
                       {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                       lemma17-2 T'
                                 ([v:ctriv]app_stack (APP v)) 
                                 (VVE v1 vvv1) 
                                 ([v:ctriv]app_stack (APP1 v))
                                 ([v:ctriv]vvalMS_v (VVMS v)) 
                                 (DSE v1 dsv1)
                                 (DSE' v1 dsv1). 

lemma17-2_cret_v : lemma17-2 T
                             ([v:ctriv]app_init)
                             ([v:ctriv][vvv]vval_cret VVC (vvv XXi))
                             ([v:ctriv]app_init)
                             VVMS
                             ([v:ctriv][dsv]
                               dstack_subst_cret DSC (dsv Xi v))
                             ([v:ctriv][dsv]
                               dstack_subst_cret DSC (dsv Xi (T v))).


lemma17-2_capp_t0_v : {t0:ctriv}
                      {dst0:{xi:stack}dstack_substT t0 xi t0 xi}
                      {vvt0:{xi:stack}vvalT xi t0 xi}
                      lemma17-2 T
                                ([v:ctriv]app_init)
                                ([v:ctriv][vvv]
                                  vval_capp VVC (vvt0 XXi) (vvv XXi))
                                ([v:ctriv]app_init)
                                VVMS
                                ([v:ctriv][dsv]
                                  dstack_subst_capp DSC 
                                                    (dst0 Xi) 
                                                    (dsv Xi v))
                                ([v:ctriv][dsv]
                                  dstack_subst_capp DSC 
                                                    (dst0 Xi) (dsv Xi (T v))).


lemma17-2_capp_v0_v_c : {v0:ctriv}
                        {dsv0:{xi:stack}{t:ctriv}
                              dstack_substT v0 (xi , t) t xi}
                        {vvv0:{xi:stack}vvalT (xi , v0) v0 xi}
                        lemma17-2 T
                                  ([v:ctriv]app_init)
                                  ([v:ctriv][vvv]
                                    vval_capp VVC (vvv0 XXi) (vvv (XXi , v0)))
                                  ([v:ctriv]app_init)
                                  (VVMS v0)
                                  ([v:ctriv][dsv]
                                    dstack_subst_capp DSC 
                                                      (dsv0 Xi T0) 
                                                      (dsv (Xi , T0) v))
                                  ([v:ctriv][dsv]
                                    dstack_subst_capp DSC 
                                                      (dsv0 Xi T0) 
                                                      (dsv (Xi , T0) (T v))).


lemma17-2_capp_v0_v1_c : ({v0:ctriv}
                          {dsv0:{xi:stack}{t:ctriv}
                                dstack_substT v0 (xi , t) t xi}
                          {vvv0:{xi:stack}vvalT (xi , v0) v0 xi}
                          {v1:ctriv}
                          {dsv1:{xi:stack}{t:ctriv}
                                dstack_substT v1 (xi , t) t xi}
                          {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                          lemma17-2 T
                                    ([v:ctriv]app_stack (app_stack (APP v)))
                                    ([v:ctriv][vvv]
                                      vval_capp (vval_vlam [v2:ctriv][vvv2]
                                                           (VVE v2 vvv2 v vvv))
                                                (vvv0 (XXi v)) 
                                                (vvv1 ((XXi v) , v0)))
                                   ([v:ctriv]app_stack (app_stack (APP1 v)))
                                   (VVMS v0 v1)
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp 
                                      (dstack_subst_vlam [v2:ctriv][dsv2]
                                                          (DSE v2 dsv2 v dsv))
                                      (dsv0 (Xi v) (T'' v0))
                                      (dsv1 ((Xi v) , (T'' v0)) (T' v1)))
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp 
                                      (dstack_subst_vlam [v2:ctriv][dsv2]
                                                          (DSE' v2 dsv2 v dsv))
                                      (dsv0 (Xi (T v)) (T'' v0))
                                      (dsv1 ((Xi (T v)) , (T'' v0)) (T' v1))))
                    <- ({v:ctriv}{v1:ctriv}
                        {dsv1:{xi:stack}{t:ctriv}
                              dstack_substT v1 (xi , t) t xi}
                        {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                        {v0:ctriv}
                        www (VVMS v0 v1 v) (vvv1 ((XXi v) , v0))  
                            (dsv1 ((Xi (T v)) , (T'' v0)) (T' v1)) 
                            (VVMS' v0 v))
                    <- ({v:ctriv}{v0:ctriv}
                        {dsv0:{xi:stack}{t:ctriv}
                              dstack_substT v0 (xi , t) t xi}
                        {vvv0:{xi:stack}vvalT (xi , v0) v0 xi}
                        www (VVMS' v0 v) (vvv0 (XXi v))
                            (dsv0 (Xi (T v)) (T'' v0)) (VVMS'' v))
                    <- {v2:ctriv}
                       {dsv2:{xi:stack}{t:ctriv}dstack_substT v2 (xi , t) t xi}
                       {vvv2:{xi:stack}vvalT (xi , v2) v2 xi}
                       lemma17-2 T
                                 ([v:ctriv]app_stack (APP v)) 
                                 (VVE v2 vvv2)
                                 ([v:ctriv]app_stack (APP1 v))
                                 ([v:ctriv]vvalMS_v (VVMS'' v))
                                 (DSE v2 dsv2)
                                 (DSE' v2 dsv2).


lemma17-2_capp_t0_v1_c : ({v1:ctriv}
                          {dsv1:{xi:stack}{t:ctriv}
                               dstack_substT v1 (xi , t) t xi}
                          {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                          {t0:ctriv}
                          {dst0:{xi:stack}
                                dstack_substT t0 xi t0 xi}
                          {vvt0:{xi:stack}vvalT xi t0 xi}
                          lemma17-2 T
                                    ([v:ctriv]app_stack (APP v))
                                    ([v:ctriv][vvv]
                                      vval_capp (vval_vlam [v2:ctriv][vvv2]
                                                          (VVE v2 vvv2  v vvv))
                                                (vvt0 (XXi v))  
                                                (vvv1 (XXi v)))
                                    ([v:ctriv]app_stack (APP1 v))
                                    (VVMS v1)
                                    ([v:ctriv][dsv]
                                      dstack_subst_capp 
                                       (dstack_subst_vlam [v2:ctriv][dsv2]
                                                           (DSE v2 dsv2 v dsv))
                                       (dst0 (Xi v))
                                       (dsv1 (Xi v) (T' v1)))
                                    ([v:ctriv][dsv]
                                      dstack_subst_capp 
                                       (dstack_subst_vlam [v2:ctriv][dsv2]
                                                          (DSE' v2 dsv2 v dsv))
                                       (dst0 (Xi (T v)))
                                       (dsv1 (Xi (T v)) (T' v1))))
                    <- ({v:ctriv}{v1:ctriv}
                        {dsv1:{xi:stack}{t:ctriv}
                              dstack_substT v1 (xi , t) t xi}
                        {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                        www (VVMS v1 v) (vvv1 (XXi v)) 
                            (dsv1 (Xi (T v)) (T' v1)) (VVMS' v))
                    <- {v2:ctriv}
                       {dsv2:{xi:stack}{t:ctriv}dstack_substT v2 (xi , t) t xi}
                       {vvv2:{xi:stack}vvalT (xi , v2) v2 xi}
                       lemma17-2 T
                                 ([v:ctriv]app_stack (APP v)) 
                                 (VVE v2 vvv2)
                                 ([v:ctriv]app_stack (APP1 v))
                                 ([v:ctriv]vvalMS_v (VVMS' v))
                                 (DSE v2 dsv2)
                                 (DSE' v2 dsv2).

lemma17-2_capp_v_v1_c : {v1:ctriv}
                        {dsv1:{xi:stack}{t:ctriv}
                              dstack_substT v1 (xi , t) t xi}
                        {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                        lemma17-2 T''
                                  ([v:ctriv]app_stack (APP v))
                                  ([v:ctriv][vvv]
                                    vval_capp VVC 
                                              (vvv XXi) 
                                              (vvv1 (XXi , v)))
                                   ([v:ctriv]app_stack (APP1 v))
                                   (VVMS v1)
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp DSC
                                                       (dsv Xi v)
                                                       (dsv1 (Xi , v) (T' v1)))
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp DSC
                                                       (dsv Xi (T'' v))
                                                       (dsv1 (Xi , (T'' v)) (T' v1))).


lemmaa17-2_capp_v0_t1_c : ({v0:ctriv}
                           {dsv0:{xi:stack}{t:ctriv}
                                  dstack_substT v0 (xi , t) t xi}
                           {vvv0:{xi:stack}vvalT (xi , v0) v0 xi}
                           {t1:ctriv}
                           {dst1:{xi:stack}dstack_substT t1 xi t1 xi}
                           {vvt1:{xi:stack}vvalT xi t1 xi}
                           lemma17-2 T
                                     ([v:ctriv]app_stack (APP v))
                                    ([v:ctriv][vvv]
                                     vval_capp (vval_vlam [v1:ctriv][vvv1]
                                                           (VVC v1 vvv1 v vvv))
                                               (vvv0 (XXi v)) 
                                               (vvt1 ((XXi v) , v0)))
                                    ([v:ctriv]app_stack (APP1 v))
                                    (VVMS v0)
                                    ([v:ctriv][dsv]
                                      dstack_subst_capp 
                                       (dstack_subst_vlam [v1:ctriv][dsv1]
                                                          (DSE v1 dsv1 v dsv))
                                       (dsv0 (Xi v) (T'' v0))
                                       (dst1 ((Xi v) , (T'' v0))))
                                    ([v:ctriv][dsv]
                                      dstack_subst_capp 
                                       (dstack_subst_vlam [v1:ctriv][dsv1]
                                                           (DSE' v1 dsv1 v dsv))
                                       (dsv0 (Xi (T v)) (T'' v0))
                                       (dst1 ((Xi (T v)) , (T'' v0)))))
                    <- ({v:ctriv}{v0:ctriv}
                        {dsv0:{xi:stack}{t:ctriv}
                              dstack_substT v0 (xi , t) t xi}
                        {vvv0:{xi:stack}vvalT (xi , v0) v0 xi}
                        www (VVMS v0 v) (vvv0 (XXi v)) 
                            (dsv0 (Xi (T v)) (T'' v0)) (VVMS' v))
                           <- {v1:ctriv}
                              {dsv1:{xi:stack}{t:ctriv}
                                    dstack_substT v1 (xi , t) t xi}
                              {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                              lemma17-2 T
                                        ([v:ctriv]app_stack (APP v)) 
                                        (VVE v1 vvv1) 
                                        ([v:ctriv]app_stack (APP1 v))
                                        ([v:ctriv]vvalMS_v (VVMS' v)) 
                                        (DSE v1 dsv1)
                                        (DSE' v1 dsv1). 

lemma17-2_capp_v_t1_c : {t1:ctriv}
                        {dst1:{xi:stack}
                               dstack_substT t1 xi t1 xi}
                        {vvt1:{xi:stack}vvalT xi t1 xi}
                        lemma17-2 T
                                  ([v:ctriv]app_init)
                                  ([v:ctriv][vvv]
                                    vval_capp VVC
                                              (vvv XXi) 
                                              (vvt1 (XXi , v))) 
                                   ([v:ctriv]app_init)
                                   VVMS
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp DSC
                                                       (dsv Xi v)
                                                       (dst1 (Xi , v)))
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp DSC
                                                       (dsv Xi (T v))
                                                       (dst1 (Xi , (T v)))).

lemma17-2_capp_t0_t1_c : ({t0:ctriv}
                          {dst0:{xi:stack}
                               dstack_substT t0 xi t0 xi}
                         {vvt0:{xi:stack}vvalT xi t0 xi}
                         {t1:ctriv}
                         {dst1:{xi:stack}
                               dstack_substT t1 xi t1 xi}
                         {vvt1:{xi:stack}vvalT xi t1 xi}
                         lemma17-2 T
                                   APP
                                   ([v:ctriv][vvv]
                                     vval_capp (vval_vlam [v1:ctriv][vvv1]
                                                           (VVE v1 vvv1 v vvv))
                                               (vvt0 (XXi v)) 
                                               (vvt1 (XXi v)))
                                   APP1
                                   VVMS 
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp 
                                      (dstack_subst_vlam [v1:ctriv][dsv1]
                                                          (DSE v1 dsv1 v dsv))
                                      (dst0 (Xi v))
                                      (dst1 (Xi v)))
                                   ([v:ctriv][dsv]
                                     dstack_subst_capp 
                                      (dstack_subst_vlam [v1:ctriv][dsv1]
                                                         (DSE' v1 dsv1 v dsv))
                                      (dst0 (Xi (T v)))
                                      (dst1 (Xi (T v)))))
                    <- {v1:ctriv}
                       {dsv1:{xi:stack}{t:ctriv}dstack_substT v1 (xi , t) t xi}
                       {vvv1:{xi:stack}vvalT (xi , v1) v1 xi}
                       lemma17-2 T
                                 ([v:ctriv]app_stack (APP v)) 
                                 (VVE v1 vvv1) 
                                 ([v:ctriv]app_stack (APP1 v))
                                 ([v:ctriv]vvalMS_v (VVMS v)) 
                                 (DSE v1 dsv1)
                                 (DSE' v1 dsv1). 


v-part : vvalMS XXi Xi -> stack -> type.

v-part_init : v-part vvalMS_init dot.

v-part_v : v-part ((vvalMS_v CV):vvalMS (XXi , V) (Xi , V)) (S , V)
           <- v-part CV S.

v-part_t : v-part (vvalMS_t CV VVT) S 
           <- v-part CV S.

doubleC : vvalC XXi C -> vvalMS XXi Xi -> dstack_substC C Xi C'
          -> v-part (CV:vvalMS XXi Xi) XXi' 
          -> dstack_substC C' XXi' C' 
          -> type.

doubleE : vvalE XXi E -> vvalMS XXi Xi -> dstack_substE E Xi E'
           -> v-part (VC:vvalMS XXi Xi) XXi' 
           -> dstack_substE E' Xi' E' 
           -> type.

doubleT : vvalT XXi T XXi' 
           -> vvalMS XXi Xi
           -> dstack_substT T Xi T' Xi'
           -> v-part (CV:vvalMS XXi Xi) XXi1
           -> vvalMS XXi' Xi'
           -> v-part (CV':vvalMS XXi' Xi') XXi2
           -> dstack_substT T' XXi1 T' XXi2
           -> type.


double_vlam : doubleC (vval_vlam VVE) VVALMS (dstack_subst_vlam DSE)
                      VP (dstack_subst_vlam DSE')
               <- {v:ctriv}
                  {vvv:{xi:stack}vvalT (xi , v) v xi}
                  {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                  doubleE (VVE v vvv)
                           (vvalMS_v VVALMS)
                           (DSE v dsv)
                           (v-part_v VP)
                           (DSE' v dsv).

double_v : {v:ctriv}
           {vvv:{xi:stack}vvalT (xi , v) v xi}
           {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
           doubleT (vvv XXi) (vvalMS_v (CV:vvalMS XXi Xi)) (dsv Xi v) 
                   (v-part_v (VP:v-part CV XXi')) CV VP (dsv XXi' v).
                  
double_v' : {v:ctriv}
            {vvv:{xi:stack}vvalT (xi , v) v xi}
            {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
            doubleT (vvv XXi) (vvalMS_t (CV:vvalMS XXi Xi) VVT) 
                    (dsv Xi T) 
                    (v-part_t (VP:v-part CV XXi')) CV VP DST.

double_t : {t:ctriv}
           {vvt:{xi:stack}vvalT xi t xi}
           {dst:{xi:stack}dstack_substT t xi t xi}
           doubleT (vvt XXi) VVMS (dst Xi) VP CV VP (dst Xi).
             


double_cret : doubleE (vval_cret VVC VVT)
                        VVMS
                        (dstack_subst_cret DSC DST)
                        VP
                        (dstack_subst_cret DSC' DST')
               <- doubleT VVT VVMS DST VP VVMS' VP' DST'
               <- doubleC VVC VVMS' DSC VP' DSC'.
          

double_capp : doubleE (vval_capp VVC VVT0 VVT1)
                        VVMS
                        (dstack_subst_capp DSC DST0 DST1)
                        VP
                        (dstack_subst_capp DSC' DST0' DST1')
               <- doubleT VVT1 VVMS DST1 VP VVMS' VP' DST1'
               <- doubleT VVT0 VVMS' DST0 VP' VVMS'' VP'' DST0'
               <- doubleC VVC VVMS'' DSC VP'' DSC'.

       
vpartDS : vvalDS XXi Xi -> vvalMS XXi Xi 
          -> v-part (CV:vvalMS XXi Xi) dot -> type. 

vpartDS_init : vpartDS vvalDS_init vvalMS_init v-part_init.

vpartDS_stack : vpartDS (vvalDS_stack VVDS VVT) (vvalMS_t CV VVT) (v-part_t VP)
                <- vpartDS VVDS CV VP.

lemma17-3_cret_k : lemma17-3 ([k:ccont][vvk]vval_cret vvk VVT)
                             (cval_cret cval_k CVT)
                             VVC
                             VVMS
                             VVDS
                             APP
                             DSC
                             (dstack_subst_cret DSC' DST')
                             (dstack_subst_cret DSC DST)
                    <- vpartDS VVDS VVMS' VP
                    <- doubleC VVC VVMS' DSC VP DSC'
                    <- lappT DST' APP app_init DST.

lemma17-3_cret_vlam : lemma17-3 ([k:ccont][vvk]
                                  vval_cret (vval_vlam [v:ctriv][vvv]
                                                        VVE v vvv k vvk)
                                            VVT)
                                (cval_cret (cval_vlam CVE) CVT)
                                VVC1
                                VVMS
                                VVDS
                                APP
                                DSC1
                                (dstack_subst_cret (dstack_subst_vlam DSE') 
                                                   DST')
                                (dstack_subst_cret (dstack_subst_vlam DSE) DST)
                      <- lappT DST' APP APP' DST
                      <- www VVMS VVT DST' VVMS'
                      <- {v:ctriv}
                         {vvv:{xi:stack}vvalT (xi , v) v xi}
                         {cvv:cvalT v}
                         {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                         lemma17-3 (VVE v vvv)
                                   (CVE v cvv)
                                   VVC1
                                   (vvalMS_v VVMS')
                                   VVDS
                                   (app_stack APP')
                                   DSC1
                                   (DSE' v dsv)
                                   (DSE v dsv).

lemma17-3_capp_k : lemma17-3 ([k:ccont][vvk]vval_capp vvk VVT1 VVT0)
                             (cval_capp cval_k CVT1 CVT0)
                             VVC
                             VVMS
                             VVDS
                             APP
                             DSC
                             (dstack_subst_capp DSC' DST0' DST1')
                             (dstack_subst_capp DSC DST0 DST1)
                    <- vpartDS VVDS VVMS' VP
                    <- doubleC VVC VVMS' DSC VP DSC'
                    <- lappT DST1' APP APP' DST1
                    <- lappT DST0' APP' app_init DST0.

lemma17-3_capp_vlam : lemma17-3 ([k:ccont][vvk]
                                  vval_capp (vval_vlam [v:ctriv][vvv]
                                                        VVE v vvv k vvk)
                                            VVT0 VVT1)
                                (cval_capp (cval_vlam CVE) CVT1 CVT0)
                                VVC1
                                VVMS
                                VVDS
                                APP
                                DSC1
                                (dstack_subst_capp (dstack_subst_vlam DSE') 
                                                   DST0' 
                                                   DST1')
                                (dstack_subst_capp (dstack_subst_vlam DSE) 
                                                   DST0
                                                   DST1)
                      <- lappT DST1' APP APP' DST1
                      <- www VVMS VVT1 DST1' VVMS'
                      <- lappT DST0' APP' APP'' DST0
                      <- www VVMS' VVT0 DST0' VVMS''
                      <- {v:ctriv}
                         {vvv:{xi:stack}vvalT (xi , v) v xi}
                         {cvv:cvalT v}
                         {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
                         lemma17-3 (VVE v vvv)
                                   (CVE v cvv)
                                   VVC1
                                   (vvalMS_v VVMS'')
                                   VVDS
                                   (app_stack APP'')
                                   DSC1
                                   (DSE' v dsv)
                                   (DSE v dsv).




rsT : vvalT XXi T XXi' 
      -> cvalT T 
      -> vvalDS XXi Xi 
      -> cvalDS Xi 
      -> dstack_substT T Xi T' Xi' 
      -> ({xi:stack}vvalT xi T' xi) 
      -> cvalT T' 
      -> vvalDS XXi' Xi' 
      -> cvalDS Xi' 
      -> ({xi:stack}dstack_substT T' xi T' xi) 
      -> type.

rs_v : {v:ctriv}
       {vvv:{xi:stack}vvalT (xi , v) v xi}
       {cvv:cvalT v}
       {dsv:{xi:stack}{t:ctriv}dstack_substT v (xi , t) t xi}
       rsT (vvv XXi) cvv (vvalDS_stack VVDS VVT') (cvalDS_stack CVDS CVT') 
           (dsv Xi T) VVT' CVT' VVDS CVDS DST'
       <- rsT (VVT' XXi) CVT' VVDS CVDS (DST' Xi)
              VVT' CVT' VVDS CVDS DST'. 

rs_t : {t:ctriv}
       {vvt:{xi:stack}vvalT xi t xi}
       {cvt:cvalT t}
       {dst:{xi:stack}dstack_substT t xi t xi}
       rsT (vvt XXi) cvt VVDS CVDS (dst Xi) vvt cvt VVDS CVDS dst.

clr : ({k:ccont}{vvk:vvalC dot k}vvalE dot (E k)) 
      -> cvalE E 
      -> vvalC XXi' C
      -> vvalDS XXi' Xi'
      -> dstack_substC C Xi' C'
      -> dstack_substE (E C) Xi' (E C') 
      -> type.

clr_proof : clr VVE CVE VVC VVDS DSC DSE
            <- vpartDS VVDS VVMS VP
            <- doubleC VVC VVMS DSC VP DSC'
            <- lemma17-1C VVC' DSC'
            <- lemma17-1E (VVE C' VVC') DSE'
            <- lemma17-3 VVE CVE VVC vvalMS_init VVDS app_init 
                         DSC DSE' DSE.