proposition: Lemma refine_if_Then_Else_Duplicate {A} : forall (i : bool) (t e e' : Comp A), refine (if i then (if i then t else e') else e) (if i then t else e).
proof: Proof. destruct i; simpl; 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