proposition: Lemma refine_skip2 {A B} (a : Comp A) (dummy : Comp B) : refine a (dummy>> a).
proof: Proof. repeat first [ intro | computes_to_inv | assumption | econstructor; eassumption | econstructor; try eassumption; [] ]. eauto. 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