proposition: Lemma Is_true_iff_eq_true : forall b, Is_true b <-> b = true.
proof: Proof. split ; intro. - apply Is_true_eq_true; assumption. - apply Is_true_eq_left; assumption. Qed.
imports: Cdcl.Formula Cdcl.ReifClasses Cdcl.ZArithDec Lia List Uint63 Cdcl.Formula Bool