fact: Definition and_cf {A} (cf: cond_and_flag) (c: condition A) := let c := if cf.(cf_negate_next) then cond_negate c else c in {| cf_cond := combine_conditions andb cf.(cf_cond) c; cf_negate_next := false |}.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core Coq.Vectors.Vector