proposition: Lemma t_interp_wf : forall i, t_interp.[i] = interp_aux (PArray.get t_interp) (t_atom.[i]).
proof: Proof. intros i;case_eq (i <? PArray.length t_atom);intros. apply t_interp_wf_lt;trivial. rewrite !PArray.get_outofbound;trivial. rewrite default_t_atom, default_t_interp;trivial. rewrite length_t_interp;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList