fact: Definition _shl_lit_be (a: list _lit) : list _lit := match a with | [] => [] | _ => Lit._false :: removelast a end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance