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 "static_2/relocation/drops.ma".
16 include "basic_2/dynamic/lsubv.ma".
18 (* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
20 (* Properties with generic slicing for local environments *******************)
22 (* Note: the premise 𝐔⦃f⦄ cannot be removed *)
23 (* Basic_2A1: includes: lsubsv_drop_O1_conf *)
24 lemma lsubv_drops_conf_isuni (a) (h) (G):
25 ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
26 ∀b,f,K1. 𝐔⦃f⦄ → ⬇*[b,f] L1 ≘ K1 →
27 ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L2 ≘ K2.
28 #a #h #G #L1 #L2 #H elim H -L1 -L2
29 [ /2 width=3 by ex2_intro/
30 | #I #L1 #L2 #HL12 #IH #b #f #K1 #Hf #H
31 elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
33 /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
34 | #g #Hg #HLK1 #H destruct -HL12
35 elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
37 | #L1 #L2 #W #V #HVW #HL12 #IH #b #f #K1 #Hf #H
38 elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
40 /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
41 | #g #Hg #HLK1 #H destruct -HL12
42 elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
47 (* Note: the premise 𝐔⦃f⦄ cannot be removed *)
48 (* Basic_2A1: includes: lsubsv_drop_O1_trans *)
49 lemma lsubv_drops_trans_isuni (a) (h) (G):
50 ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
51 ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2 →
52 ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & ⬇*[b,f] L1 ≘ K1.
53 #a #h #G #L1 #L2 #H elim H -L1 -L2
54 [ /2 width=3 by ex2_intro/
55 | #I #L1 #L2 #HL12 #IH #b #f #K2 #Hf #H
56 elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
58 /3 width=3 by lsubv_bind, drops_refl, ex2_intro/
59 | #g #Hg #HLK2 #H destruct -HL12
60 elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
62 | #L1 #L2 #W #V #HWV #HL12 #IH #b #f #K2 #Hf #H
63 elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
65 /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
66 | #g #Hg #HLK2 #H destruct -HL12
67 elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/