@iref_eq_repl
@(subset_eq_canc_sn ā¦ (lift_term_grafted_S ā¦))
@lift_term_eq_repl_sn
+(* š ¢[f]p ā ā*[ā(m+n)]š ¢[f](((pāš)āb)āšāq) *)
(* Note: crux of the proof begins *)
>lift_rmap_A_dx
/2 width=2 by tls_succ_plus_lift_rmap_append_closed_bLq_dx/