proposition: Lemma valid_check_trans : forall res eqs, C.interp rho (check_trans res eqs).
proof: Proof. unfold check_trans;intros res [ | leq eqs]. - apply get_eq_interp;intros. destruct (Misc.reflect_eqb a b). + unfold C.interp; simpl; rewrite orb_false_r. unfold Lit.interp; simpl; rewrite Lit.is_pos_lit. unfold Var.interp; simpl; rewrite Lit.blit_lit. rewrite H1. unfold Atom.interp_bool; simpl. rewrite e; simpl. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H3. rewrite H3. intros [vb HHb]. unfold Atom.interp_hatom. rewrite HHb;simpl;rewrite Typ.cast_refl;simpl. apply Typ.i_eqb_refl. + auto with smtcoq_euf. - apply get_eq_interp;intros. apply check_trans_aux_correct with t;trivial. simpl;rewrite Lit.interp_nlit;unfold Var.interp. rewrite <- H1. destruct (rho (Lit.blit leq));auto with smtcoq_core. Qed.
imports: Bool List Int63 PArray State SMT_terms