proposition: Lemma eval_pexprSC : forall env s, eval_sexpr env s = eval_pexpr env (map_PExpr s).
proof: Proof. unfold eval_pexpr, eval_sexpr. intros env s; induction s as [| |? IHs1 ? IHs2|? IHs1 ? IHs2|? IHs1 ? IHs2|? IHs|? IHs ?]; simpl ; try (rewrite IHs1 ; rewrite IHs2) ; try reflexivity. - apply phi_C_of_S. - rewrite IHs. reflexivity. - rewrite IHs. reflexivity. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl