qed.
lemma modularm: ∀R.∀L:vlattice R.∀y,z:L. μ(y∧z) ≈ μy + μz + -μ (y ∨ z).
+(* CSC: questa è la causa per cui la hint per cercare i duplicati ci sta 1 mese *)
+(* exact modularj; *)
intros (R L y z);
lapply (modular_mjp ?? y z) as H1;
apply (plus_cancl ??? (μ(y ∨ z)));