proposition: Lemma flip_flip_REv {E1 E2} REv1: @eq_REv E1 E2 (flip_REv (flip_REv REv1)) REv1.
proof: Proof. reflexivity. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)