proposition: Lemma build_congr_correct : forall lp l r c, (Forall2 _ _ (fun a b => interp_hatom a = interp_hatom b) l r -> C.interp rho c) -> C.interp rho (build_congr lp l r c).
proof: Proof. induction lp;destruct l;destruct r;simpl;trivial with smtcoq_euf smtcoq_core;intros. apply H;constructor. destruct a. apply get_eq_interp;intros. match goal with |- context [if ?x then _ else _] => case_eq x;intros;auto with smtcoq_euf smtcoq_core end. apply IHlp;simpl;intros. rewrite Lit.interp_nlit;unfold Var.interp. case_eq (rho (Lit.blit i1));intros;simpl;[ | auto with smtcoq_euf smtcoq_core]. apply H;constructor;trivial with smtcoq_euf smtcoq_core. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H3. rewrite Typ.eqb_spec in H4. unfold Atom.get_type in H3, H4. rewrite H3,H4. intros [va HHa] [vb HHb]. revert H7;rewrite H2;unfold Atom.apply_binop; simpl. unfold Atom.interp_hatom. rewrite HHa, HHb;simpl;rewrite Typ.cast_refl;simpl. intros W;change (is_true (Typ.i_eqb t_i t va vb)) in W. rewrite Typ.i_eqb_spec in W. rewrite orb_true_iff, !andb_true_iff in H5;destruct H5 as [ [H5 H7] | [H5 H7]]. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. rewrite eqb_spec in H5. rewrite eqb_spec in H7. subst. rewrite HHa, HHb;trivial with smtcoq_euf smtcoq_core. destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. apply IHlp;intros;apply H;constructor;auto with smtcoq_euf smtcoq_core. Qed.
imports: Bool List Int63 PArray State SMT_terms