proposition: Lemma refine_trivial_if_then_else : forall x, refine (If_Then_Else x (ret true) (ret false)) (ret x).
proof: Proof. destruct x; reflexivity. Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Bool.Bool Fiat.Common Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Computation.Core Fiat.Computation.Monad Fiat.Computation.SetoidMorphisms Fiat.Computation.Refinements.Tactics