1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2A/substitution/drop_lreq.ma".
16 include "basic_2A/multiple/frees.ma".
18 (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
20 (* Properties on equivalence for local environments *************************)
22 lemma lreq_frees_trans: āL2,U,l,i. L2 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā
23 āL1. L1 ā©¬[l, ā] L2 ā L1 ā¢ i Ļµ š
*[l]ā¦Uā¦.
24 #L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/
25 #I2 #L2 #K2 #U #W2 #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW2 #L1 #HL12
26 elim (lreq_drop_trans_be ā¦ HL12 ā¦ HLK2) -L2 // >yminus_Y_inj #K1 #HK12 #HLK1
27 lapply (lreq_inv_O_Y ā¦ HK12) -HK12 #H destruct /3 width=9 by frees_be/
30 lemma frees_lreq_conf: āL1,U,l,i. L1 ā¢ i Ļµ š
*[l]ā¦Uā¦ ā
31 āL2. L1 ā©¬[l, ā] L2 ā L2 ā¢ i Ļµ š
*[l]ā¦Uā¦.
32 /3 width=3 by lreq_sym, lreq_frees_trans/ qed-.