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/equivalence/cpcs_cpcs.ma".
16 include "basic_2/dynamic/lsubsn.ma".
18 (* LOCAL ENVIRONMENT REFINEMENT FOR STRATIFIED NATIVE TYPE ASSIGNMENT *******)
20 (* Properties on context-sensitive parallel equivalence for terms ***********)
22 lemma cpr_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
23 ∀T1,T2. L2 ⊢ T1 ➡ T2 → L1 ⊢ T1 ➡ T2.
24 /3 width=5 by lsubsn_fwd_lsubs2, cpr_lsubs_trans/ qed-.
26 lemma cprs_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
27 ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
28 /3 width=5 by lsubsn_fwd_lsubs2, cprs_lsubs_trans/ qed-.
30 lemma cpcs_lsubsn_trans: ∀h,L1,L2. h ⊢ L1 :⊑[] L2 →
31 ∀T1,T2. L2 ⊢ T1 ⬌* T2 → L1 ⊢ T1 ⬌* T2.
32 /3 width=5 by lsubsn_fwd_lsubs2, cpcs_lsubs_trans/ qed-.