proposition: Lemma reflect_cop_eqb : forall o1 o2, reflect (o1 = o2) (cop_eqb o1 o2).
proof: Proof. destruct o1; destruct o2; simpl; try (constructor; trivial; discriminate). apply iff_reflect. split. intro. inversion H. rewrite andb_true_iff. split. rewrite N.eqb_refl; auto. apply RAWBITVECTOR_LIST.List_eq_refl; auto. intros. rewrite andb_true_iff in H. destruct H as (Ha, Hb). apply N.eqb_eq in Ha. rewrite RAWBITVECTOR_LIST.List_eq in Hb. now rewrite Ha, Hb. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList