DEFINITION subst0_weight_le()
TYPE =
       ∀u:T
         .∀t:T
           .∀z:T
             .∀d:nat
               .subst0 d u t z
                 →∀f:nat→nat
                      .∀g:nat→nat
                        .∀m:nat.(le (f m) (g m))
                          →(lt (weight_map f (lift (S d) O u)) (g d)
                               →le (weight_map f z) (weight_map g t))
BODY =
Show proof