proposition: Lemma rutt_trigger {E1 E2 R1 R2 REv RAns RR} (e1: E1 R1) (e2: E2 R2): (REv _ _ e1 e2: Prop) -> (forall t1 t2, (RAns _ _ e1 t1 e2 t2: Prop) -> (RR t1 t2: Prop)) -> rutt REv RAns RR (trigger e1) (trigger e2).
proof: Proof. intros. apply rutt_Vis; auto. intros. apply rutt_Ret; auto. Qed.
imports: Coq(Program Setoid Morphisms RelationClasses) Paco(paco) ITree(ITree ITreeFacts Core.Subevent Basics.HeterogeneousRelations Eq.Rutt Props.Leaf)