proposition: Lemma is_true_eq : forall b, is_true b <-> Is_true b.
proof: Proof. unfold is_true. destruct b; simpl; intuition congruence. Qed.
imports: Cdcl.Itauto Uint63 Bool ZArith Lia Coq.Lists.List Coq.ZArith.ZArith Coq.micromega.Lia Bool ZifyClasses Coq.ZArith.ZArith Coq.micromega.Lia Classical