proposition: Lemma rel_in_fun_of_fun_in_rel_functional : forall f R, fun_in_rel f R -> functional R -> rel_in_fun R f.
proof: Proof. Proof using. introv h1 h2. intros a b H. forwards M: h1 a. forwards*: h2 H M. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)