+ 'CircledTimes p = (structure p).
+
+(* Basic constructions ******************************************************)
+
+lemma structure_empty:
+ π = βπ.
+// qed.
+
+lemma structure_d_sn (p) (n):
+ βp = β(π±β¨nβ©βp).
+// qed.
+
+lemma structure_L_sn (p):
+ πββp = β(πβp).
+// qed.
+
+lemma structure_A_sn (p):
+ πββp = β(πβp).
+// qed.
+
+lemma structure_S_sn (p):
+ π¦ββp = β(π¦βp).
+// qed.
+
+(* Main constructions *******************************************************)
+
+theorem structure_idem (p):
+ βp = ββp.
+#p elim p -p [| * [ #n ] #p #IH ] //
+qed.
+
+theorem structure_append (p1) (p2):
+ βp1ββp2 = β(p1βp2).
+#p1 elim p1 -p1 [| * [ #n ] #p1 #IH ] #p2
+[||*: <list_append_lcons_sn ] //
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma structure_d_dx (p) (n):
+ βp = β(pβπ±β¨nβ©).
+#p #n <structure_append //
+qed.
+
+lemma structure_L_dx (p):
+ (βp)βπ = β(pβπ).
+#p <structure_append //
+qed.
+
+lemma structure_A_dx (p):
+ (βp)βπ = β(pβπ).
+#p <structure_append //
+qed.
+
+lemma structure_S_dx (p):
+ (βp)βπ¦ = β(pβπ¦).
+#p <structure_append //
+qed.