DEFINITION csubv_bind_same()
TYPE =
       ∀c1:C
         .∀c2:C
           .csubv c1 c2
             →∀b:B.∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2))
BODY =
        assume c1: C
        assume c2: C
        suppose H: csubv c1 c2
        assume b: B
          we proceed by induction on b to prove ∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2))
             case Abbr : ⇒
                the thesis becomes ∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Abbr) v1) (CHead c2 (Bind Abbr) v2))
                    assume v1: T
                    assume v2: T
                      we must prove not (eq B Abbr Void)
                      or equivalently (eq B Abbr Void)→False
                      suppose H0: eq B Abbr Void
                         by (not_abbr_void H0)
                         we proved False
                      we proved (eq B Abbr Void)→False
                      that is equivalent to not (eq B Abbr Void)
                      by (csubv_bind . . H . previous . . .)
                      we proved csubv (CHead c1 (Bind Abbr) v1) (CHead c2 (Bind Abbr) v2)
∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Abbr) v1) (CHead c2 (Bind Abbr) v2))
             case Abst : ⇒
                the thesis becomes ∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Abst) v1) (CHead c2 (Bind Abst) v2))
                    assume v1: T
                    assume v2: T
                      by (sym_not_eq . . . not_void_abst)
                      we proved not (eq B Abst Void)
                      by (csubv_bind . . H . previous . . .)
                      we proved csubv (CHead c1 (Bind Abst) v1) (CHead c2 (Bind Abst) v2)
∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Abst) v1) (CHead c2 (Bind Abst) v2))
             case Void : ⇒
                the thesis becomes ∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Void) v1) (CHead c2 (Bind Void) v2))
                    assume v1: T
                    assume v2: T
                      by (csubv_void . . H . .)
                      we proved csubv (CHead c1 (Bind Void) v1) (CHead c2 (Bind Void) v2)
∀v1:T.∀v2:T.(csubv (CHead c1 (Bind Void) v1) (CHead c2 (Bind Void) v2))
          we proved ∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2))
       we proved 
          ∀c1:C
            .∀c2:C
              .csubv c1 c2
                →∀b:B.∀v1:T.∀v2:T.(csubv (CHead c1 (Bind b) v1) (CHead c2 (Bind b) v2))