proposition: Lemma reflect_uop_eqb : forall o1 o2, reflect (o1 = o2) (uop_eqb o1 o2).
proof: Proof. intros [ | | | | | s1 n1 | s1 | s1 | s1 | s1 | s1 ] [ | | | | |s2 n2 | s2 | s2 | s2 | s2 | s2 ];simpl; try constructor;trivial; try discriminate. - apply iff_reflect. case_eq (Nat.eqb n1 n2). + case_eq ((s1 =? s2)%N). * rewrite N.eqb_eq, beq_nat_true_iff. intros -> ->. split; reflexivity. * rewrite N.eqb_neq, beq_nat_true_iff. intros H1 ->; split; try discriminate. intro H. inversion H. elim H1. auto. + split; auto. * rewrite beq_nat_false_iff in H. intros. contradict H0. intro H'. apply H. inversion H'. reflexivity. * intros. contradict H0. easy. - apply iff_reflect. rewrite N.eqb_eq. split; intro H. + now inversion H. + now rewrite H. - apply iff_reflect. rewrite N.eqb_eq. split; intro H. + now inversion H. + now rewrite H. - intros. apply iff_reflect. split. intro H. inversion H. rewrite !andb_true_iff; split. split; now rewrite N.eqb_eq. now rewrite N.eqb_eq. intros. rewrite !andb_true_iff in H. destruct H as ((Ha, Hb), Hc). rewrite N.eqb_eq in Ha, Hb, Hc. subst. reflexivity. - intros. apply iff_reflect. split; intros. + rewrite !andb_true_iff. inversion H. split; try split; try now rewrite N.eqb_eq. + rewrite !andb_true_iff in H. destruct H as (Ha, Hb). rewrite N.eqb_eq in Ha, Hb. now subst. - intros. apply iff_reflect. split; intros. + rewrite !andb_true_iff. inversion H. split; try split; try now rewrite N.eqb_eq. + rewrite !andb_true_iff in H. destruct H as (Ha, Hb). rewrite N.eqb_eq in Ha, Hb. now subst. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList