DEFINITION lift_free()
TYPE =
       ∀t:T
         .∀h:nat
           .∀k:nat
             .∀d:nat
               .∀e:nat
                 .le e (plus d h)
                   →(le d e)→(eq T (lift k e (lift h d t)) (lift (plus k h) d t))
BODY =
       assume t: T
          we proceed by induction on t to prove 
             ∀h:nat
               .∀k:nat
                 .∀d:nat
                   .∀e:nat
                     .le e (plus d h)
                       →(le d e)→(eq T (lift k e (lift h d t)) (lift (plus k h) d t))
             case TSort : n:nat ⇒
                the thesis becomes 
                ∀h:nat
                  .∀k:nat
                    .∀d:nat
                      .∀e:nat
                        .le e (plus d h)
                          →(le d e
                               →(eq
                                    T
                                    lift k e (lift h d (TSort n))
                                    lift (plus k h) d (TSort n)))
                    assume h: nat
                    assume k: nat
                    assume d: nat
                    assume e: nat
                    suppose : le e (plus d h)
                    suppose : le d e
                      (h1) 
                         (h1) 
                            (h1) 
                               by (refl_equal . .)
eq T (TSort n) (TSort n)
                            end of h1
                            (h2) 
                               by (lift_sort . . .)
eq T (lift (plus k h) d (TSort n)) (TSort n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
eq T (TSort n) (lift (plus k h) d (TSort n))
                         end of h1
                         (h2) 
                            by (lift_sort . . .)
eq T (lift k e (TSort n)) (TSort n)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
eq T (lift k e (TSort n)) (lift (plus k h) d (TSort n))
                      end of h1
                      (h2) 
                         by (lift_sort . . .)
eq T (lift h d (TSort n)) (TSort n)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift k e (lift h d (TSort n))
                           lift (plus k h) d (TSort n)

                      ∀h:nat
                        .∀k:nat
                          .∀d:nat
                            .∀e:nat
                              .le e (plus d h)
                                →(le d e
                                     →(eq
                                          T
                                          lift k e (lift h d (TSort n))
                                          lift (plus k h) d (TSort n)))
             case TLRef : n:nat ⇒
                the thesis becomes 
                ∀h:nat
                  .∀k:nat
                    .∀d:nat
                      .∀e:nat
                        .∀H:le e (plus d h)
                          .∀H0:le d e
                            .eq
                              T
                              lift k e (lift h d (TLRef n))
                              lift (plus k h) d (TLRef n)
                    assume h: nat
                    assume k: nat
                    assume d: nat
                    assume e: nat
                    suppose H: le e (plus d h)
                    suppose H0: le d e
                      (h1) 
                         suppose H1: lt n d
                            (h1) 
                               (h1) 
                                  (h1) 
                                     by (refl_equal . .)
eq T (TLRef n) (TLRef n)
                                  end of h1
                                  (h2) 
                                     by (lift_lref_lt . . . H1)
eq T (lift (plus k h) d (TLRef n)) (TLRef n)
                                  end of h2
                                  by (eq_ind_r . . . h1 . h2)
eq T (TLRef n) (lift (plus k h) d (TLRef n))
                               end of h1
                               (h2) 
                                  by (lt_le_trans . . . H1 H0)
                                  we proved lt n e
                                  by (lift_lref_lt . . . previous)
eq T (lift k e (TLRef n)) (TLRef n)
                               end of h2
                               by (eq_ind_r . . . h1 . h2)
eq T (lift k e (TLRef n)) (lift (plus k h) d (TLRef n))
                            end of h1
                            (h2) 
                               by (lift_lref_lt . . . H1)
eq T (lift h d (TLRef n)) (TLRef n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved 
                               eq
                                 T
                                 lift k e (lift h d (TLRef n))
                                 lift (plus k h) d (TLRef n)

                            lt n d
                              →(eq
                                   T
                                   lift k e (lift h d (TLRef n))
                                   lift (plus k h) d (TLRef n))
                      end of h1
                      (h2) 
                         suppose H1: le d n
                            (h1) 
                               (h1) 
                                  (h1) 
                                     by (plus_permute_2_in_3_assoc . . .)
                                     we proved eq nat (plus (plus n h) k) (plus n (plus k h))
                                     by (f_equal . . . . . previous)

                                        eq
                                          T
                                          TLRef (plus (plus n h) k)
                                          TLRef (plus n (plus k h))
                                  end of h1
                                  (h2) 
                                     by (lift_lref_ge . . . H1)

                                        eq
                                          T
                                          lift (plus k h) d (TLRef n)
                                          TLRef (plus n (plus k h))
                                  end of h2
                                  by (eq_ind_r . . . h1 . h2)

                                     eq
                                       T
                                       TLRef (plus (plus n h) k)
                                       lift (plus k h) d (TLRef n)
                               end of h1
                               (h2) 
                                  by (le_n .)
                                  we proved le h h
                                  by (le_plus_plus . . . . H1 previous)
                                  we proved le (plus d h) (plus n h)
                                  by (le_trans . . . H previous)
                                  we proved le e (plus n h)
                                  by (lift_lref_ge . . . previous)

                                     eq
                                       T
                                       lift k e (TLRef (plus n h))
                                       TLRef (plus (plus n h) k)
                               end of h2
                               by (eq_ind_r . . . h1 . h2)

                                  eq
                                    T
                                    lift k e (TLRef (plus n h))
                                    lift (plus k h) d (TLRef n)
                            end of h1
                            (h2) 
                               by (lift_lref_ge . . . H1)
eq T (lift h d (TLRef n)) (TLRef (plus n h))
                            end of h2
                            by (eq_ind_r . . . h1 . h2)
                            we proved 
                               eq
                                 T
                                 lift k e (lift h d (TLRef n))
                                 lift (plus k h) d (TLRef n)

                            le d n
                              →(eq
                                   T
                                   lift k e (lift h d (TLRef n))
                                   lift (plus k h) d (TLRef n))
                      end of h2
                      by (lt_le_e . . . h1 h2)
                      we proved 
                         eq
                           T
                           lift k e (lift h d (TLRef n))
                           lift (plus k h) d (TLRef n)

                      ∀h:nat
                        .∀k:nat
                          .∀d:nat
                            .∀e:nat
                              .∀H:le e (plus d h)
                                .∀H0:le d e
                                  .eq
                                    T
                                    lift k e (lift h d (TLRef n))
                                    lift (plus k h) d (TLRef n)
             case THead : k:K t0:T t1:T ⇒
                the thesis becomes 
                ∀h:nat
                  .∀k0:nat
                    .∀d:nat
                      .∀e:nat
                        .∀H1:le e (plus d h)
                          .∀H2:le d e
                            .eq
                              T
                              lift k0 e (lift h d (THead k t0 t1))
                              lift (plus k0 h) d (THead k t0 t1)
                (H) by induction hypothesis we know 
                   ∀h:nat
                     .∀k0:nat
                       .∀d:nat
                         .∀e:nat
                           .le e (plus d h)
                             →(le d e)→(eq T (lift k0 e (lift h d t0)) (lift (plus k0 h) d t0))
                (H0) by induction hypothesis we know 
                   ∀h:nat
                     .∀k0:nat
                       .∀d:nat
                         .∀e:nat
                           .le e (plus d h)
                             →(le d e)→(eq T (lift k0 e (lift h d t1)) (lift (plus k0 h) d t1))
                    assume h: nat
                    assume k0: nat
                    assume d: nat
                    assume e: nat
                    suppose H1: le e (plus d h)
                    suppose H2: le d e
                      (h1) 
                         (h1) 
                            (h1) 
                               (h1) 
                                  by (refl_equal . .)
eq K k k
                               end of h1
                               (h2) 
                                  by (H . . . . H1 H2)
eq T (lift k0 e (lift h d t0)) (lift (plus k0 h) d t0)
                               end of h2
                               (h3) 
                                  (h1) 
                                     by (s_plus . . .)
                                     we proved eq nat (s k (plus d h)) (plus (s k d) h)
                                     we proceed by induction on the previous result to prove le (s k e) (plus (s k d) h)
                                        case refl_equal : ⇒
                                           the thesis becomes le (s k e) (s k (plus d h))
                                              by (s_le . . . H1)
le (s k e) (s k (plus d h))
le (s k e) (plus (s k d) h)
                                  end of h1
                                  (h2) 
                                     by (s_le . . . H2)
le (s k d) (s k e)
                                  end of h2
                                  by (H0 . . . . h1 h2)
eq T (lift k0 (s k e) (lift h (s k d) t1)) (lift (plus k0 h) (s k d) t1)
                               end of h3
                               by (f_equal3 . . . . . . . . . . . h1 h2 h3)

                                  eq
                                    T
                                    THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
                                    THead k (lift (plus k0 h) d t0) (lift (plus k0 h) (s k d) t1)
                            end of h1
                            (h2) 
                               by (lift_head . . . . .)

                                  eq
                                    T
                                    lift (plus k0 h) d (THead k t0 t1)
                                    THead k (lift (plus k0 h) d t0) (lift (plus k0 h) (s k d) t1)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)

                               eq
                                 T
                                 THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
                                 lift (plus k0 h) d (THead k t0 t1)
                         end of h1
                         (h2) 
                            by (lift_head . . . . .)

                               eq
                                 T
                                 lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))
                                 THead k (lift k0 e (lift h d t0)) (lift k0 (s k e) (lift h (s k d) t1))
                         end of h2
                         by (eq_ind_r . . . h1 . h2)

                            eq
                              T
                              lift k0 e (THead k (lift h d t0) (lift h (s k d) t1))
                              lift (plus k0 h) d (THead k t0 t1)
                      end of h1
                      (h2) 
                         by (lift_head . . . . .)

                            eq
                              T
                              lift h d (THead k t0 t1)
                              THead k (lift h d t0) (lift h (s k d) t1)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
                      we proved 
                         eq
                           T
                           lift k0 e (lift h d (THead k t0 t1))
                           lift (plus k0 h) d (THead k t0 t1)

                      ∀h:nat
                        .∀k0:nat
                          .∀d:nat
                            .∀e:nat
                              .∀H1:le e (plus d h)
                                .∀H2:le d e
                                  .eq
                                    T
                                    lift k0 e (lift h d (THead k t0 t1))
                                    lift (plus k0 h) d (THead k t0 t1)
          we proved 
             ∀h:nat
               .∀k:nat
                 .∀d:nat
                   .∀e:nat
                     .le e (plus d h)
                       →(le d e)→(eq T (lift k e (lift h d t)) (lift (plus k h) d t))
       we proved 
          ∀t:T
            .∀h:nat
              .∀k:nat
                .∀d:nat
                  .∀e:nat
                    .le e (plus d h)
                      →(le d e)→(eq T (lift k e (lift h d t)) (lift (plus k h) d t))