proposition: Lemma wf_interp_form_lt : forall t_form, wf t_form -> forall x, x <? PArray.length t_form -> interp_state_var t_form x = interp t_form (t_form.[x]).
proof: Proof. unfold interp_state_var;intros. apply t_interp_wf;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList