proposition: Lemma rutt_inv_Tau t1 t2 : rutt REv RAns RR (Tau t1) (Tau t2) -> rutt REv RAns RR t1 t2.
proof: Proof. intros; apply rutt_inv_Tau_r, rutt_inv_Tau_l; assumption. Qed.
imports: Coq(Morphisms ) ExtLib(Structures.Monad) ITree(Basics.Utils Axioms ITree Eq Basics ) Paco(paco)