theorem structure_idem (p):
⊗p = ⊗⊗p.
-#p elim p -p [| * [ #k ] #p #IH ] //
+#p elim p -p //
+* [ #k ] #p #IH //
qed.
theorem structure_append (p) (q):
⊗p●⊗q = ⊗(p●q).
-#p #q elim q -q [| * [ #k ] #q #IH ]
-[||*: <list_append_lcons_sn ] //
+#p #q elim q -q //
+* [ #k ] #q #IH //
+<list_append_lcons_sn //
qed.
(* Constructions with path_lcons ********************************************)
lemma structure_d_sn (p) (k):
⊗p = ⊗(𝗱k◗p).
-#p #n <structure_append //
+#p #k <structure_append //
qed.
lemma structure_m_sn (p):