(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "basic_2/notation/relations/isidentity_2.ma".
include "basic_2/static/frees.ma".

(* FREE VARIABLES IDENTITY FOR RESTRICTED CLOSURES **************************)

definition fid: relation2 … ≝ λL,T.
                ∀f. L ⊢ 𝐅*⦃T⦄ ≡ f →  𝐈⦃f⦄.

interpretation "free variables identity (restricted closure)"
   'IsIdentity L T = (fid L T).

(* Basic properties *********************************************************)

lemma fid_sort: ∀L,s. 𝐈⦃L, ⋆s⦄.
/2 width=3 by frees_inv_sort/ qed.

lemma fid_gref: ∀L,l. 𝐈⦃L, §l⦄.
/2 width=3 by frees_inv_gref/ qed.