proposition: Fact lb_meet_left x : x↓nil ≂ nil.
proof: Proof. unfold lb_meet. split; try (constructor; fail). rewrite lb_pointwise_left. induction x as [ | [] x ]; simpl; constructor; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)