evaluation for context-sensitive extended substitution (cpye) completed!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / cpye.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma
index c93e64972fed771eb38c2bb5af2cdcd64d5ad6a4..82a1e3b4653777d2c516879270563274ce54b088 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpye.ma
@@ -57,4 +57,26 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma 
\ No newline at end of file
+lemma cpye_inv_sort1: ∀G,L,X,d,e,k. ⦃G, L⦄ ⊢ ⋆k ▶*[d, e] 𝐍⦃X⦄ → X = ⋆k.
+#G #L #X #d #e #k * /2 width=5 by cpys_inv_sort1/
+qed-.
+
+lemma cpye_inv_gref1: ∀G,L,X,d,e,p. ⦃G, L⦄ ⊢ §p ▶*[d, e] 𝐍⦃X⦄ → X = §p.
+#G #L #X #d #e #p * /2 width=5 by cpys_inv_gref1/
+qed-.
+
+lemma cpye_inv_bind1: ∀a,I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓑ{a,I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ▶*[⫯d, e] 𝐍⦃T2⦄ &
+                               X = ⓑ{a,I}V2.T2.
+#a #I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_bind1 … H1) -H1
+#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_bind … H2) -H2
+/5 width=8 by lsuby_cny_conf, lsuby_succ, ex3_2_intro, conj/
+qed-.
+
+lemma cpye_inv_flat1: ∀I,G,L,V1,T1,X,d,e. ⦃G, L⦄ ⊢ ⓕ{I}V1.T1 ▶*[d, e] 𝐍⦃X⦄ →
+                      ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ▶*[d, e] 𝐍⦃V2⦄ & ⦃G, L⦄ ⊢ T1 ▶*[d, e] 𝐍⦃T2⦄ &
+                               X = ⓕ{I}V2.T2.
+#I #G #L #V1 #T1 #X #d #e * #H1 #H2 elim (cpys_inv_flat1 … H1) -H1
+#V2 #T2 #HV12 #HT12 #H destruct elim (cny_inv_flat … H2) -H2
+/3 width=5 by ex3_2_intro, conj/
+qed-.