proposition: Theorem branching_bit_sym: forall k1 k2, branching_bit k1 k2 = branching_bit k2 k1.
proof: Proof. unfold branching_bit; intros; f_equal. eapply testbit_spec; intros. rewrite ! lxor_spec. eapply xorb_comm. Qed.
imports: Lia Cdcl.Coqlib