+
+(* Constructions with list_rcons ********************************************)
+
+lemma depth_d_dx (p) (n):
+ āpā = āpāš±nā.
+// qed.
+
+lemma depth_m_dx (p):
+ āpā = āpāšŗā.
+// qed.
+
+lemma depth_L_dx (p):
+ āāpā = āpāšā.
+// qed.
+
+lemma depth_A_dx (p):
+ āpā = āpāšā.
+// qed.
+
+lemma depth_S_dx (p):
+ āpā = āpāš¦ā.
+// qed.