proposition: Lemma rel_incl_rel_fun_eq_fun_in_rel : forall f R, rel_incl (rel_fun f) R = fun_in_rel f R.
proof: Proof. Proof using. extens. unfold rel_fun, fun_in_rel. iff H; intros x; specializes H x. { applys* H. } { intros y Hy. subst~. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)