defeq simp lemmas:
#2, g ?M_1 ?M_2 ↦ h ?M_2
#4, d ?M_1 ?M_2 ?M_3 ?M_4 ↦ f (f ?M_1 ?M_2 ?M_3) (f ?M_2 ?M_3 ?M_4) (f ?M_1 ?M_4 ?M_3)
#3, f ?M_1 ?M_2 ?M_3 ↦ g (g ?M_1 ?M_2) ?M_3
#1, h ?M_1 ↦ q ?M_1