(* Basic_2A1: includes: drop_fwd_lw_lt *)
lemma drops_fwd_lw_lt: ∀f,L1,L2. ⇩*[Ⓣ,f] L1 ≘ L2 →
- (ð\9d\90\88â\9dªfâ\9d« → ⊥) → ♯❨L2❩ < ♯❨L1❩.
+ (ð\9d\90\88â\9d¨fâ\9d© → ⊥) → ♯❨L2❩ < ♯❨L1❩.
#f #L1 #L2 #H elim H -f -L1 -L2
[ #f #Hf #Hnf elim Hnf -Hnf /2 width=1 by/
| /3 width=3 by drops_fwd_lw, nle_nlt_trans/