@(subset_eq_trans โฆ (lift_term_after โฆ))
@(subset_eq_canc_dx โฆ (lift_term_after โฆ))
@lift_term_eq_repl_sn
+(* ๐ฎโจ โ(๐ ข[f](pโ๐โb)๏ผ โจmโฉ + ๐ ข[f](pโ๐โbโ๐โq)๏ผ ยงโจnโฉ) โฉ โ ๐ ข[f]p โ ๐ ข[f](pโ๐โbโ๐โq) โ ๐ฎโจโ(m+n)โฉ *)
(* Note: crux of the proof begins *)
@(stream_eq_trans โฆ (tr_compose_uni_dx_pap โฆ)) <tr_pap_succ_nap
@tr_compose_eq_repl