proposition: Lemma Aeval_sound: forall s S a, ST.In s S -> V.In (aeval a s) (Aeval a S).
proof: Proof. induction a; cbn; intros. - apply V.const_1. - apply H. - apply V.add_1; auto. - apply V.sub_1; auto. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) CDF(Sequences IMP)