λδ-2B is released

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / lsubr_drops.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma
index 4009cdd2988d51e4ab08d4e44b0024e05358a537..9876c8fd2dfce995d011343711fed4e3a789c794 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubr_drops.ma
@@ -20,11 +20,12 @@ include "static_2/static/lsubr.ma".
 (* Forward lemmas with generic slicing for local environments ***************)
 
 (* Basic_2A1: includes: lsubr_fwd_drop2_pair *)
-lemma lsubr_fwd_drops2_bind: ∀L1,L2. L1 ⫃ L2 → 
-                             ∀b,f,I,K2. 𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓘ{I} →
-                             ∨∨ ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓘ{I}
-                              | ∃∃K1,W,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W
-                              | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2.
+lemma lsubr_fwd_drops2_bind:
+      ∀L1,L2. L1 ⫃ L2 →
+      ∀b,f,I,K2. 𝐔⦃f⦄ → ⇩*[b,f] L2 ≘ K2.ⓘ{I} →
+      ∨∨ ∃∃K1. K1 ⫃ K2 & ⇩*[b,f] L1 ≘ K1.ⓘ{I}
+       | ∃∃K1,W,V. K1 ⫃ K2 & ⇩*[b,f] L1 ≘ K1.ⓓⓝW.V & I = BPair Abst W
+       | ∃∃J1,J2,K1,V. K1 ⫃ K2 & ⇩*[b,f] L1 ≘ K1.ⓑ{J1}V & I = BUnit J2.
 #L1 #L2 #H elim H -L1 -L2
 [ #b #f #I #K2 #_ #H
   elim (drops_inv_atom1 … H) -H #H destruct
@@ -41,9 +42,10 @@ elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
 qed-.
 
 (* Basic_2A1: includes: lsubr_fwd_drop2_abbr *)
-lemma lsubr_fwd_drops2_abbr: ∀L1,L2. L1 ⫃ L2 →
-                             ∀b,f,K2,V.  𝐔⦃f⦄ → ⬇*[b,f] L2 ≘ K2.ⓓV →
-                             ∃∃K1. K1 ⫃ K2 & ⬇*[b,f] L1 ≘ K1.ⓓV.
+lemma lsubr_fwd_drops2_abbr:
+      ∀L1,L2. L1 ⫃ L2 →
+      ∀b,f,K2,V. 𝐔⦃f⦄ → ⇩*[b,f] L2 ≘ K2.ⓓV →
+      ∃∃K1. K1 ⫃ K2 & ⇩*[b,f] L1 ≘ K1.ⓓV.
 #L1 #L2 #HL12 #b #f #K2 #V #Hf #HLK2
 elim (lsubr_fwd_drops2_bind … HL12 … Hf HLK2) -L2 -Hf // *
 [ #K1 #W #V #_ #_ #H destruct