fact: Fixpoint lform_app (o:lop) (acc : list (HCons.t LForm)) (l: list (HCons.t LForm)) := match l with | nil => acc | e :: l => match e.(elt) with | LOP o' l' => if lop_eqb o o' then lform_app o (rev_append l' acc) l else lform_app o (e::acc) l | _ => lform_app o (e::acc) l end end.
imports: Cdcl.PatriciaR Cdcl.KeyInt Cdcl.ReifClasses Cdcl.Lib Bool Setoid ZifyBool ZArith Uint63 Lia List Cdcl.Syntax Cdcl.Clause