-apply (le_transitive ????? (ml_prop2 ?? ml (y) ??));
- cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
- apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
- lapply (le_to_eqm ??? Lxy) as Dxm;
- lapply (le_to_eqm ??? Lyz) as Dym;
- lapply (le_to_eqj ??? Lxy) as Dxj;
- lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
- apply (eq_trans ?? (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
- apply (eq_trans ?? (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
- apply (eq_trans ?? ? ? (plus_comm ???));
- apply (eq_trans ?? (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
- apply feq_plusl;
- apply (eq_trans ?? (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
- apply eq_reflexive;
+apply (le_transitive ????? (ml_prop2 ?? (y) ??));
+cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
+ apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
+lapply (le_to_eqm ??? Lxy) as Dxm; lapply (le_to_eqm ??? Lyz) as Dym;
+lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
+apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
+apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z) (meq_l ????? Dxj));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [
+ apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (x∨y) ? Dyj));]
+apply (Eq≈ ? (plus_comm ???));
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y)));
+apply feq_plusl;
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ?x y)));
+apply eq_reflexive;