<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f โฆ Ht2) -Ht2 #Ht2 -Ht1
@(subset_eq_trans โฆ Ht2) -t2
@(subset_eq_trans โฆ (lift_term_fsubst โฆ))
@fsubst_eq_repl [ // | // ]
<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f โฆ Ht2) -Ht2 #Ht2 -Ht1
@(subset_eq_trans โฆ Ht2) -t2
@(subset_eq_trans โฆ (lift_term_fsubst โฆ))
@fsubst_eq_repl [ // | // ]