proposition: Lemma valid_get : forall rho s, valid rho s -> forall id, C.valid rho (get s id).
proof: Proof. intros rho s H id. unfold valid in H. unfold Valuation.t in rho. apply H. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring