proposition: Lemma check_aux_interp_hatom_lt : forall h, h <? length t_atom -> exists v, t_interp.[h] = Bval (get_type h) v.
proof: Proof. assert (Bt := to_Z_bounded (length t_atom)). set (P' i t := length t = length t_atom -> forall j, j <? i -> exists v, t.[j] = Bval (v_type Typ.type interp_t (t.[j])) v). assert (P' (length t_atom) t_interp). unfold t_interp;apply foldi_ind;unfold P';intros. rewrite leb_spec, to_Z_0; lia. elim (ltb_0 _ H0). rewrite length_set in H2. destruct (Misc.reflect_eqb j i). rewrite e, PArray.get_set_same. apply check_aux_interp_aux_lt; auto. rewrite H2; auto. assert (j <? i). assert ([|j|] <> [|i|]) by(intros Heq1;elim n;apply to_Z_inj;trivial). generalize H3;unfold is_true;rewrite !ltb_spec, (to_Z_add_1 _ _ H0);auto with zarith. rewrite get_set_other;auto. apply H;apply length_t_interp. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList