[ /2 width=3 by subset_in_eq_repl_back/
| /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
]
[ /2 width=3 by subset_in_eq_repl_back/
| /5 width=3 by subset_eq_canc_sn, fsubst_eq_repl, lift_term_eq_repl_dx, grafted_eq_repl/
]