proposition: Lemma valid_internal_set : forall rho s, valid rho s -> forall c, C.valid rho c -> forall id, valid rho (set s id c).
proof: Proof. unfold valid, get;simpl;intros. destruct (reflect_eqb id id0);subst. case_eq (id0 <? length s);intros. rewrite PArray.get_set_same;trivial. rewrite PArray.get_outofbound. rewrite PArray.default_set. rewrite <- (PArray.get_outofbound _ _ (length s)); trivial. rewrite <- not_true_iff_false, ltb_spec;auto with zarith. rewrite PArray.length_set;trivial. rewrite get_set_other;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring