proposition: Lemma flip_flip_RAns {E1 E2} (RAns: forall A B, E1 A -> A -> E2 B -> B -> Prop): eq_RAns (flip_RAns (flip_RAns RAns)) RAns.
proof: Proof. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)