@(subset_eq_canc_sn β¦ (lift_term_eq_repl_dx β¦))
[ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
@(subset_eq_trans β¦ (lift_unwind2_term_after β¦))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
<list_append_rcons_sn
@(subset_eq_canc_sn β¦ (lift_term_eq_repl_dx β¦))
[ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
@(subset_eq_trans β¦ (lift_unwind2_term_after β¦))
@unwind2_term_eq_repl_sn
(* Note: crux of the proof begins *)
<list_append_rcons_sn