proposition: Lemma refine_If_Then_Else' : forall (A : Type) (c : bool) (x x0 y y0 : Comp A), (c = true -> refine x y) -> (c = false -> refine x0 y0) -> refine (If c Then x Else x0) (If c Then y Else y0).
proof: Proof. unfold refine; intros; destruct c; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements String_as_OT FMapAVL