lemma depth_S_sn (q): āqā = āš¦āqā.
// qed.
-(* Advanced constructions with nplus ****************************************)
+(* Main constructions *******************************************************)
-lemma depth_plus (p1) (p2):
- āp2ā+āp1ā = āp1āp2ā.
+theorem depth_append (p1) (p2):
+ āp2ā+āp1ā = āp1āp2ā.
#p1 elim p1 -p1 //
* [ #n ] #p1 #IH #p2 <list_append_lcons_sn
[ <depth_d_sn <depth_d_sn //
| <depth_S_sn <depth_S_sn //
]
qed.
+
+(* 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.