lapply (modular_mjp ?? x (y ∧ z)) as H1;
apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
apply (eq_trans ?? ? ?? (plus_comm ???));
lapply (modular_mjp ?? x (y ∧ z)) as H1;
apply (eq_trans ?? (μ(x∧(y∧z))+ μ(x∨(y∧z)) +-μ(x∧(y∧z)))); [2: apply feq_plusr; apply (eq_trans ???? (plus_comm ???)); apply H1] clear H1;
apply (eq_trans ?? ? ?? (plus_comm ???));