+lemma depth_A_dx (p):
+ ♭p = ♭(p◖𝗔).
+// qed.
+
+lemma depth_S_dx (p):
+ ♭p = ♭(p◖𝗦).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem depth_append (p) (q):
+ (♭p)+(♭q) = ♭(p●q).
+#p #q elim q -q //
+* [ #k | #k #d ] #q #IH <list_append_lcons_sn
+[ <depth_d_dx <depth_d_dx //
+| <depth_d2_dx <depth_d2_dx //
+| <depth_m_dx <depth_m_dx //
+| <depth_L_dx <depth_L_dx //
+| <depth_A_dx <depth_A_dx //
+| <depth_S_dx <depth_S_dx //
+]
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma depth_d_sn (p) (k):
+ ♭p = ♭(𝗱k◗p).
+// qed.
+
+lemma depth_d2_sn (p) (k) (d):
+ ♭p = ♭(𝗱❨k,d❩◗p).
+// qed.
+
+lemma depth_m_sn (p):
+ ♭p = ♭(𝗺◗p).
+// qed.
+
+lemma depth_L_sn (p):
+ ↑♭p = ♭(𝗟◗p).
+// qed.
+
+lemma depth_A_sn (p):
+ ♭p = ♭(𝗔◗p).
+// qed.
+
+lemma depth_S_sn (p):
+ ♭p = ♭(𝗦◗p).