+| <lift_path_m_sn #H
+ elim (IH ā¦ H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+ /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+ (šŗāq) = ā[f]p ā ā„.
+#q #p @(path_ind_lift ā¦ p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/