proposition: Lemma refinement_step {A} (c c' : Comp A) : refine c c' -> Refinement of c' -> Refinement of c.
proof: Proof. intros refine_c_c' Refinement_c'. destruct Refinement_c' as [c'' refine_c'_c'']. intros; econstructor. etransitivity; eassumption. Defined.
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