-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 y x Lxy) as Dxm; lapply (le_to_eqm z y Lyz) as Dym;
+lapply (le_to_eqj x y Lxy) as Dxj; lapply (le_to_eqj y z Lyz) as Dyj; clear Lxy Lyz;
+STOP
+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) + δ(y∨x) z));[
+ apply feq_plusl; apply meq_l; clear Dyj Dxm Dym; assumption]
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(y∨x) (z∨y))); [
+ apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (y∨x) ? Dyj));]
+apply (Eq≈ ? (plus_comm ???));
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)));[
+ apply feq_plusr; apply meq_r; apply (join_comm ??);]
+apply feq_plusl;
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ??)));
+apply eq_reflexive;