proposition: Lemma rel_to_fun_eq_of_functional : forall x y R, functional R -> R x y -> rel_to_fun R x = y.
proof: Proof. Proof using IB. introv M E. applys* rel_in_fun_rel_to_fun. Qed.
imports: TLC(LibTactics LibLogic LibRelation)