-| <structure_d2_dx #H0 /2 width=1 by/
-| <structure_m_dx #H0 /2 width=1 by/
-| <structure_L_dx #H0 destruct
-| <structure_A_dx #H0 destruct
-| <structure_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_d2_dx_structure (d) (h) (q) (p):
- qāš±āØh,dā© = āp ā ā„.
-#d #h #q #p elim p -p [| * [ #k | #k #d ] #p #IH ]
-[ <structure_empty #H0 destruct
-| <structure_d_dx #H0 /2 width=1 by/
-| <structure_d2_dx #H0 /2 width=1 by/