proposition: Lemma refine_If_Opt_Then_Else_cond {A B} : forall (c : option B) (e e': Comp A) (t t' : B -> Comp A), (forall b, c = Some b -> refine (t b) (t' b)) -> (c = None -> refine e e') -> refine (Ifopt c as b' Then t b' Else e) (Ifopt c as b' Then t' b' Else e').
proof: Proof. intros; destruct c; simpl in *; eauto. Qed.
imports: Fiat.QueryStructure.Automation.MasterPlan Bedrock.Memory