proposition: Lemma rutt_add_Tau_r t1 t2 : rutt REv RAns RR t1 t2 -> rutt REv RAns RR t1 (Tau t2).
proof: Proof. intros. pfold. red. cbn. constructor. pstep_reverse. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)