fact: Definition eval_ite (k:kind) (o:ite) : bool -> eval_kind k -> eval_kind k -> eval_kind k := fun (b:bool) e1 e2 => if b then e1 else e2.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause