DEFINITION lift_gen_bind()
TYPE =
       ∀b:B
         .∀u:T
           .∀t:T
             .∀x:T
               .∀h:nat
                 .∀d:nat
                   .eq T (THead (Bind b) u t) (lift h d x)
                     →(ex3_2
                          T
                          T
                          λy:T.λz:T.eq T x (THead (Bind b) y z)
                          λy:T.λ:T.eq T u (lift h d y)
                          λ:T.λz:T.eq T t (lift h (S d) z))
BODY =
        assume b: B
        assume u: T
        assume t: T
        assume x: T
        assume h: nat
        assume d: nat
        suppose H: eq T (THead (Bind b) u t) (lift h d x)
          (H_x) 
             by (lift_gen_head . . . . . . H)

                ex3_2
                  T
                  T
                  λy:T.λz:T.eq T x (THead (Bind b) y z)
                  λy:T.λ:T.eq T u (lift h d y)
                  λ:T.λz:T.eq T t (lift h (s (Bind b) d) z)
          end of H_x
          (H0) consider H_x
          consider H0
          we proved 
             ex3_2
               T
               T
               λy:T.λz:T.eq T x (THead (Bind b) y z)
               λy:T.λ:T.eq T u (lift h d y)
               λ:T.λz:T.eq T t (lift h (s (Bind b) d) z)
          that is equivalent to 
             ex3_2
               T
               T
               λy:T.λz:T.eq T x (THead (Bind b) y z)
               λy:T.λ:T.eq T u (lift h d y)
               λ:T.λz:T.eq T t (lift h (S d) z)
          we proceed by induction on the previous result to prove 
             ex3_2
               T
               T
               λy:T.λz:T.eq T x (THead (Bind b) y z)
               λy:T.λ:T.eq T u (lift h d y)
               λ:T.λz:T.eq T t (lift h (S d) z)
             case ex3_2_intro : x0:T x1:T H1:eq T x (THead (Bind b) x0 x1) H2:eq T u (lift h d x0) H3:eq T t (lift h (S d) x1) ⇒
                the thesis becomes 
                ex3_2
                  T
                  T
                  λy:T.λz:T.eq T x (THead (Bind b) y z)
                  λy:T.λ:T.eq T u (lift h d y)
                  λ:T.λz:T.eq T t (lift h (S d) z)
                   (h1) 
                      by (refl_equal . .)
eq T (THead (Bind b) x0 x1) (THead (Bind b) x0 x1)
                   end of h1
                   (h2) 
                      by (refl_equal . .)
eq T (lift h d x0) (lift h d x0)
                   end of h2
                   (h3) 
                      by (refl_equal . .)
eq T (lift h (S d) x1) (lift h (S d) x1)
                   end of h3
                   by (ex3_2_intro . . . . . . . h1 h2 h3)
                   we proved 
                      ex3_2
                        T
                        T
                        λy:T.λz:T.eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)
                        λy:T.λ:T.eq T (lift h d x0) (lift h d y)
                        λ:T.λz:T.eq T (lift h (S d) x1) (lift h (S d) z)
                   by (eq_ind_r . . . previous . H2)
                   we proved 
                      ex3_2
                        T
                        T
                        λy:T.λz:T.eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)
                        λy:T.λ:T.eq T u (lift h d y)
                        λ:T.λz:T.eq T (lift h (S d) x1) (lift h (S d) z)
                   by (eq_ind_r . . . previous . H3)
                   we proved 
                      ex3_2
                        T
                        T
                        λy:T.λz:T.eq T (THead (Bind b) x0 x1) (THead (Bind b) y z)
                        λy:T.λ:T.eq T u (lift h d y)
                        λ:T.λz:T.eq T t (lift h (S d) z)
                   by (eq_ind_r . . . previous . H1)

                      ex3_2
                        T
                        T
                        λy:T.λz:T.eq T x (THead (Bind b) y z)
                        λy:T.λ:T.eq T u (lift h d y)
                        λ:T.λz:T.eq T t (lift h (S d) z)
          we proved 
             ex3_2
               T
               T
               λy:T.λz:T.eq T x (THead (Bind b) y z)
               λy:T.λ:T.eq T u (lift h d y)
               λ:T.λz:T.eq T t (lift h (S d) z)
       we proved 
          ∀b:B
            .∀u:T
              .∀t:T
                .∀x:T
                  .∀h:nat
                    .∀d:nat
                      .eq T (THead (Bind b) u t) (lift h d x)
                        →(ex3_2
                             T
                             T
                             λy:T.λz:T.eq T x (THead (Bind b) y z)
                             λy:T.λ:T.eq T u (lift h d y)
                             λ:T.λz:T.eq T t (lift h (S d) z))