(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.
(* FREE VARIABLES INCLUSION FOR RESTRICTED CLOSURES *************************)
definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.