proposition: Lemma check_aux_interp_hatom : forall h, exists v, t_interp.[h] = Bval (get_type h) v.
proof: Proof. intros i;case_eq (i <? PArray.length t_atom);intros. apply check_aux_interp_hatom_lt;trivial. unfold get_type'; rewrite !PArray.get_outofbound;trivial. rewrite default_t_interp; simpl; exists (1%positive); auto. rewrite length_t_interp;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList