#[global]
Instance Proper_apply_IFun {E F : Type → Type} {T : Type}
         (RE : ∀ T, E T → E T → Prop)
         (RF : ∀ T, F T → F T → Prop)
  : Proper (i_respectful RE RF ==> RE T ==> RF T) apply_IFun.
Proof.
  repeat red; eauto.
Qed.

Lemma fold_apply_IFun {E F : Type → Type} {T : Type}
  : ∀ (f : E ~> F) (t : E T),
    f _ t = apply_IFun f t.
Proof.
  reflexivity.
Qed.