@(subset_eq_canc_sn … (lift_term_grafted_S …))
@lift_term_eq_repl_sn
(* Note: crux of the proof begins *)
- /2 width=2 by tls_succ_lift_rmap_append_L_closed_dx/
+ /2 width=2 by tls_succ_lift_rmap_append_closed_Lq_dx/
(* Note: crux of the proof ends *)
]
qed.