fact: Definition lt_atom i a := match a with | Acop _ => true | Auop _ h => h <? i | Abop _ h1 h2 => (h1 <? i) && (h2 <? i) | Atop _ h1 h2 h3 => (h1 <? i) && (h2 <? i) && (h3 <? i) | Anop _ ha => List.forallb (fun h => h <? i) ha | Aapp f args => List.forallb (fun h => h <? i) args end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList