proposition: Lemma eval_formulaSC : forall env f, eval_sformula env f = eval_formula env (map_Formula f).
proof: Proof. intros env f; destruct f. simpl. repeat rewrite eval_pexprSC. reflexivity. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl