proposition: Lemma SharpenIfComputesTo {A} : forall (cond : bool) (cT cE : Comp A) vT vE, cT ↝ vT -> cE ↝ vE -> (if cond then cT else cE) ↝ if cond then vT else vE.
proof: Proof. destruct cond; eauto. Qed.
imports: Coq.Lists.List Coq.Arith.Arith Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADT.ComputationalADT Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTNotation.BuildADTReplaceMethods Fiat.ADTRefinement.Core Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.BuildADTSetoidMorphisms Coq.Strings.String