proposition: Lemma eqitF_VisF_gen {E R1 R2} {RR : R1 -> R2 -> Prop} {b1 b2 vclo sim} {X1 X2} (p : X1 = X2) (e1 : E X1) (k1 : X1 -> _) (e2 : E X2) (k2 : X2 -> _) : eqeq E p e1 e2 -> pweqeq (vclo sim) p k1 k2 -> eqitF RR b1 b2 vclo sim (VisF e1 k1) (VisF e2 k2).
proof: Proof. destruct p; intros <-; cbn; constructor; auto. Qed.
imports: Coq(Structures.Orders Program Setoid Morphisms Relations) Paco(paco) ITree(Basics.Basics Basics.Utils Basics.HeterogeneousRelations Core.ITreeDefinition Eq.Paco2 Eq.Shallow)