proposition: Lemma functional_of_rel_in_fun : forall R f, rel_in_fun R f -> functional R.
proof: Proof. Proof using. unfold rel_in_fun, functional. introv M N1 N2. lets: M N1. lets: M N2. congruence. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)