proposition: Lemma is_true_isTrueExpr: forall {av} {gallinaTest : bool} {tmp : StringMap.key} (st' : State av), is_true st' (isTrueExpr tmp) -> StringMap.MapsTo tmp (wrap (bool2w gallinaTest)) st' -> gallinaTest = true.
proof: Proof. unfold isTrueExpr, bool2w, is_true, is_false, eval_bool; simpl; destruct gallinaTest; SameValues_Facade_t. Qed.
imports: CertifiedExtraction.StringMapUtils CertifiedExtraction.ExtendedLemmas CertifiedExtraction.Extraction.Core CertifiedExtraction.Extraction.Basics