proposition: Lemma ite1 : forall (b:bool) (p1 p2:Prop), (if b then p1 else p2) <-> ((b = true -> p1) /\ (b = true \/ p2)).
proof: Proof. destruct b ; intuition congruence. Qed.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause