proposition: Lemma list_beq_compute_interp : forall t l1 l2, list_beq check_hatom l1 l2 = true -> forall acc, compute_interp t_i (interp_hatom t_i t_func t_atom) t acc l1 = compute_interp t_i (interp_hatom t_i t_func t_atom) t acc l2.
proof: Proof. intro t; induction l1 as [ |h1 l1 IHl1]; intros [ |h2 l2]; simpl; try discriminate; auto; rewrite andb_true_iff; intros [H1 H2] acc; rewrite (check_hatom_correct _ _ H1); destruct (interp_hatom t_i t_func t_atom h2) as [ta va]; destruct (Typ.cast ta t) as [ka| ]; auto. Qed.
imports: List PArray Bool Int63 ZMicromega ZArith Misc State SMT_terms BVList