proposition: Lemma eq_bool_intro : forall (x y:bool), (x = true <-> y = true) <-> x = y.
proof: Proof. destruct x,y; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause