proposition: Lemma interp_binop_eqb_trans: forall u a b c, Typ.eqb (get_type a) u -> Typ.eqb (get_type b) u -> Typ.eqb (get_type c) u -> Atom.interp_bool t_i (Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) (interp_hatom a) (interp_hatom b)) -> Atom.interp_bool t_i (Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) (interp_hatom b) (interp_hatom c)) -> Atom.interp_bool t_i (Atom.apply_binop t_i u u Typ.Tbool (Typ.i_eqb t_i u) (interp_hatom a) (interp_hatom c)).
proof: Proof. intros u a b c Ha Hb Hc. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom c). rewrite Typ.eqb_spec in Ha. rewrite Typ.eqb_spec in Hb. rewrite Typ.eqb_spec in Hc. unfold Atom.get_type in Ha, Hb, Hc. rewrite Ha, Hb, Hc. intros [va HHa] [vb HHb] [vc HHc]. unfold Atom.interp_hatom. rewrite HHa, HHb, HHc;simpl;rewrite Typ.cast_refl. unfold Atom.interp_bool;simpl. apply Typ.i_eqb_trans. Qed.
imports: Bool List Int63 PArray State SMT_terms