| lapply (in_comp_lift_path_term f ā¦ Ht1) -Ht2 -Ht1 -H1n
<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f ā¦ Ht2) -Ht2 #Ht2 -Ht1
| lapply (in_comp_lift_path_term f ā¦ Ht1) -Ht2 -Ht1 -H1n
<lift_path_d_dx #Ht1 //
| lapply (lift_term_eq_repl_dx f ā¦ Ht2) -Ht2 #Ht2 -Ht1