proposition: Lemma rel_in_fun_rel_to_fun : forall R, functional R -> rel_in_fun R (rel_to_fun R).
proof: Proof. Proof using IB. unfold rel_in_fun, rel_to_fun. introv M H. epsilon* z. Qed.
imports: TLC(LibTactics LibLogic LibRelation)