proposition: Lemma fold_apply_IFun {E F : Type -> Type} {T : Type} : forall (f : E ~> F) (t : E T), f _ t = apply_IFun f t.
proof: Proof. reflexivity. Qed.
imports: Coq(Setoid Morphisms) ITree(Basics.Basics Indexed.Function Indexed.Relation)