proposition: Fact lb_join_nil_eq a b : a↑b ≂ nil -> a ≂ nil /\ b ≂ nil.
proof: Proof. intros H; split. rewrite <- (lb_meet_left a), <- H, lb_meet_join_idem; auto. rewrite <- (lb_meet_left b), <- H, lb_join_comm, lb_meet_join_idem; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)