-(* apply (eq_trans ?? (0+μ(x∧(y∧z))) ?? (opp_inverse ??)); ASSERT FALSE *)
-apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z)))); [2: apply eq_sym; apply plus_assoc;]
-apply (eq_trans ?? (0+μ(x∧(y∨z)))); [2: apply feq_plusr; apply eq_sym; apply opp_inverse;]
-(* apply (eq_trans ?? ? ? (eq_refl ??) (zero_neutral ??)); ASSERT FALSE *)
-apply (eq_trans ?? (μ(x∧(y∨z)))); [apply eq_reflexive]
-apply eq_sym; apply zero_neutral.
+apply (eq_trans ?? (- μ(x∨(y∨z))+ μ(x∨(y∨z))+ μ(x∧(y∨z))) ?? (plus_assoc ????));
+apply (eq_trans ?? (0+μ(x∧(y∨z))) ?? (opp_inverse ??));
+apply (eq_trans ?? (μ(x∧(y∨z))) ?? (zero_neutral ??));
+apply eq_reflexive.