proposition: Lemma wf_interp_form : forall t_form, PArray.default t_form = Ftrue -> wf t_form -> forall x, interp_state_var t_form x = interp t_form (t_form.[x]).
proof: Proof. intros t Hd Hwf x;case_eq (x <? PArray.length t);intros. apply wf_interp_form_lt;trivial. unfold interp_state_var;rewrite !PArray.get_outofbound;trivial. rewrite default_t_interp, Hd;trivial. rewrite length_t_interp;trivial. Qed.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList