proposition: Fact lb_join_left x : x↑nil = x.
proof: Proof. unfold lb_join. rewrite lb_pointwise_left. induction x as [ | [] ]; simpl; f_equal; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)