proposition: Lemma interp_lit : forall rho l, interp rho (lit (blit l)) = Var.interp rho (blit l).
proof: Proof. intros;unfold interp;rewrite is_pos_lit, blit_lit;trivial. Qed.
imports: List Bool Int63 Psatz Ring63 PArray Misc Ring