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_2/rt_transition/rpx_lpx.ma".
17 (* UNBOUND PARALLEL RT-TRANSITION FOR FULL LOCAL ENVIRONMENTS ***************)
19 (* Forward lemmas with free variables inclusion for restricted closures *****)
21 (* Basic_2A1: uses: lpx_cpx_frees_trans *)
22 lemma lpx_cpx_conf_fsge (h) (G): ∀L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 →
23 ∀L2. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃L2, T1⦄ ⊆ ⦃L0, T0⦄.
24 /3 width=4 by rpx_cpx_conf_fsge, lpx_rpx/ qed-.
26 (* Basic_2A1: uses: lpx_frees_trans *)
27 lemma lpx_fsge_comp (h) (G): ∀L0,L2,T0. ⦃G, L0⦄ ⊢ ⬈[h] L2 → ⦃L2, T0⦄ ⊆ ⦃L0, T0⦄.
28 /2 width=4 by lpx_cpx_conf_fsge/ qed-.