proposition: Lemma eqit_inv t1 t2 : eqit RR b1 b2 t1 t2 -> eqit__ t1 t2.
proof: Proof. intros H; punfold H; red in H. genobs t1 ot1; genobs t2 ot2; revert t1 t2 Heqot1 Heqot2; unfold observe, _observe. destruct H; pclearbot; intros * E1 E2; rewrite <- E1, <- E2; cbn; auto. - exists eq_refl; cbn; eauto. - rewrite CHECK in *. destruct ot2. 1,3: pfold; red; unfold observe, _observe; rewrite <- E2; assumption. 1: apply eqit_inv_Tau_r; pfold; red; unfold observe, _observe; assumption. - rewrite CHECK in *. destruct ot1. 1,3: pfold; red; unfold observe, _observe; rewrite <- E1; assumption. 1: apply eqit_inv_Tau_l; pfold; red; unfold observe, _observe; assumption. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)