proposition: Lemma isTrueExpr_is_false: forall {av} (tmp : string) (st' : State av), StringMap.MapsTo tmp (wrap (bool2w false)) st' -> is_false st' (isTrueExpr tmp).
proof: Proof. unfold isTrueExpr, is_true, is_false, eval_bool; simpl; SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics