proposition: Lemma eqitF_inv_VisF {E R1 R2} (RR : R1 -> R2 -> Prop) {b1 b2 vclo sim} X (e : E X) (k1 : X -> _) (k2 : X -> _) : eqitF RR b1 b2 vclo sim (VisF e k1) (VisF e k2) -> forall x, vclo sim (k1 x) (k2 x).
proof: Proof. intros H. dependent destruction H. 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)