-(*
- @(subset_eq_trans … (unwind2_term_fsubst …))
- [ @fsubst_eq_repl [ // | // ]
- @(subset_eq_trans … (unwind2_term_iref …))
- @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
- [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
- @(subset_eq_trans … (unwind2_lift_term_after …))
- @unwind2_term_eq_repl_sn
+ @(subset_eq_trans … (lift_term_fsubst …))
+ @fsubst_eq_repl [ // | // ]
+ @(subset_eq_trans … (lift_term_iref …))
+ @iref_eq_repl
+ @(subset_eq_canc_sn … (lift_term_grafted_S …))
+ @lift_term_eq_repl_sn