proposition: Lemma eq_trace_inv {E R} (t1 t2 : @trace E R) (H : t1 = t2) : match t1, t2 with | TEnd, TEnd => True | TRet r1, TRet r2 => r1 = r2 | TEventEnd e1, TEventEnd e2 => exists p, eqeq E p e1 e2 | TEventResponse e1 x1 t1, TEventResponse e2 x2 t2 => exists p, eqeq E p e1 e2 /\ eqeq (fun X => X) p x1 x2 /\ t1 = t2 | _, _ => False end.
proof: Proof. destruct H, t1; auto. - exists eq_refl; cbn; auto. - exists eq_refl; cbn; auto. Qed.
imports: Paco(paco) ITree(Basics.Utils Axioms Core.ITreeDefinition Eq.Eqit Eq.UpToTaus Eq.SimUpToTaus Eq.Shallow Eq.Paco2)