- @or_intror @conj [ /2 width=1 by subset_in_ext_f1_dx/ ] *
- [ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
- <list_append_empty_dx @H2p -H2p /2 width=1 by prototerm_in_comp_root/
- | #l #r #Hr
- elim (lift_inv_append_proper_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
- lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
- ]
+ @or_intror @conj [ /2 width=1 by in_comp_lift_path_term/ ] -Hq #r #Hr
+ elim (lift_path_inv_append_sn … Hr) -Hr #s1 #s2 #Hs1 #_ #H1 destruct
+ lapply (lift_path_inj … Hs1) -Hs1 #H1 destruct
+ /2 width=2 by/