proposition: Lemma eq_of_incl_defined_functional : forall R1 R2, rel_incl R1 R2 -> defined R1 -> functional R2 -> R1 = R2.
proof: Proof. Proof using. introv Hincl Hdef Hfun. extens. intros x y. iff M. { eauto. } { forwards (w'&M1): Hdef x. forwards M2: Hincl M1. forwards: Hfun M M2. subst*. } Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)