(* Basic_2A1: includes: drop_fwd_rfw *)
lemma drops_bind2_fwd_rfw: ∀b,f,I,L,K,V. ⇩*[b,f] L ≘ K.ⓑ[I]V → ∀T. ♯❨K,V❩ < ♯❨L,T❩.
#b #f #I #L #K #V #HLK lapply (drops_fwd_lw … HLK) -HLK
(* Basic_2A1: includes: drop_fwd_rfw *)
lemma drops_bind2_fwd_rfw: ∀b,f,I,L,K,V. ⇩*[b,f] L ≘ K.ⓑ[I]V → ∀T. ♯❨K,V❩ < ♯❨L,T❩.
#b #f #I #L #K #V #HLK lapply (drops_fwd_lw … HLK) -HLK