proposition: Lemma optimize_If_td2_bool {S S' T T' V} : forall (c : bool) (t e : option (S * T * V)) (k : S -> T -> V -> option (S' * T' * V)), (`(a, b, env) <- (If c Then t Else e); k a b env) = If c Then `(a, b, env) <- t; k a b env Else (`(a, b, env) <- e; k a b env).
proof: Proof. destruct c; simpl; intros; reflexivity. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache