+
+ elim Hb -Hb #Hb #H0 <H0 -H0 <nrplus_zero_dx <nplus_zero_dx <nsucc_unfold
+ >Hn
+ @(subset_eq_canc_sn โฆ (lift_term_eq_repl_dx โฆ))
+ [ @unwind_grafted_S /2 width=2 by ex_intro/ | skip ]
+ <Hn <Hn
+(*
+ @(subset_eq_trans โฆ (lift_term_eq_repl_dx โฆ))
+ [ @(unwind_term_eq_repl_sn โฆ (tls_succ_unwind q โฆ)) | skip ]
+*)