+
+(* Inversions with inner condition for path *********************************)
+
+lemma lift_inv_append_inner_sn (q1) (q2) (p) (f):
+ q1 ϵ 𝐈 → q1●q2 = ↑[f]p →
+ ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]f]p2 = q2 & p1●p2 = p.
+#q1 @(list_ind_rcons … q1) -q1
+[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
+ /2 width=5 by ex3_2_intro/
+| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
+ [ elim (pic_inv_d_dx … Hq2)
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_m_sn … (sym_eq … H2))
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
+ [ <structure_append <structure_L_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
+ [ <structure_append <structure_A_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ | <list_append_rcons_sn #H0
+ elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+ elim (lift_path_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
+ @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
+ [ <structure_append <structure_S_dx <Hr2 -Hr2 //
+ | <list_append_assoc <list_append_rcons_sn //
+ ]
+ ]
+]
+qed-.