proposition: Lemma bool_eqb_comm: forall ibs1 ibs2, Bool.eqb ibs1 ibs2 = Bool.eqb ibs2 ibs1.
proof: Proof. intros. case_eq ibs1. intros. case_eq ibs2. intros. easy. intros. easy. intros. easy. Qed.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance