proposition: Fact lb_join_idem a : a↑a = a.
proof: Proof. induction a as [ | x a ]; auto. rewrite lb_join_cons; f_equal; auto. destruct x; simpl; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)