proposition: Lemma interp_binop_eqb_sym : forall u a b, Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) a b = Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) b a.
proof: Proof. unfold Atom.apply_binop;simpl;intros u (ta,va) (tb,vb). destruct (Typ.cast ta u);destruct (Typ.cast tb u);trivial. apply f_equal; apply eq_true_iff_eq. match goal with |- ?x = _ <-> ?y = _ => change (is_true x <-> is_true y) end. split; intro; rewrite Typ.i_eqb_sym in H; auto. Qed.
imports: Bool List Int63 PArray State SMT_terms