qed.
(* Constructions with path_lcons ********************************************)
lemma structure_d_sn (p) (k):
⊗p = ⊗(𝗱k◗p).
qed.
(* Constructions with path_lcons ********************************************)
lemma structure_d_sn (p) (k):
⊗p = ⊗(𝗱k◗p).