proposition: Lemma Leaf_non_interactive_singleton : forall X (t: itree void1 X) a b, a ∈ t -> b ∈ t -> a = b.
proof: Proof. intros * IN; revert b; induction IN; intros * IN'. - rewrite itree_eta, H in IN'; apply Leaf_Ret_inv in IN'; auto. - rewrite itree_eta, H, tau_eutt in IN'; eauto. - inv e. Qed.
imports: ITree(ITree Basics.Utils Eq.Eqit Interp.TranslateFacts Leaf) ITree.Events(Nondeterminism Exception) Paco(paco) Coq(Morphisms Basics Program.Equality)