proposition: Fact lb_meet_join_distr a b c : a↓(b↑c) ≂ (a↓b)↑(a↓c).
proof: Proof. revert b c; induction a as [ | x a IHa ]; intros b c. + rew lb. + destruct b as [ | y b ]. * rew lb. * destruct c as [ | z c ]. - rew lb. - repeat rewrite lb_meet_cons. repeat rewrite lb_join_cons. repeat rewrite lb_meet_cons. apply lb_mask_equiv_cons; auto. destruct x; destruct y; destruct z; simpl; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)