+
+lemma unwind2_path_root (f) (p):
+ ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
+#f * [| * [ #k ] #p ]
+/2 width=3 by ex2_intro/
+<unwind2_path_d_dx <structure_d_dx
+/2 width=3 by ex2_intro/
+qed-.
+
+(* Destructions with structure **********************************************)
+
+lemma unwind2_path_des_structure (f) (q) (p):
+ ⊗q = ▼[f]p → ⊗q = ⊗p.
+// qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
+ q◖𝗱h = ▼[f]p →
+ ∃∃r,k. q = ⊗r & h = ▶[f]r@⧣❨k❩ & r◖𝗱k = p.
+#f #q * [| * [ #k ] #p ] #h
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_m_dx #H0
+ elim (eq_inv_d_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
+ q◖𝗺 = ▼[f]p → ⊥.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+ elim (eq_inv_m_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
+ q◖𝗟 = ▼[f]p →
+ ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+ elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
+ q◖𝗔 = ▼[f]p →
+ ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+ elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
+ q◖𝗦 = ▼[f]p →
+ ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+ elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+ /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+ /2 width=5 by ex3_2_intro/
+]
+qed-.