X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;h=4db46f940e869d38441aabd560487f600b884555;hb=6b4da5fa47d474dcf2f203ec7f5ed36938739c9b;hp=c3fa8e11bcb9000d92c76518604cf109360f305a;hpb=bd840d43d09254b41936c49fc447e58582b156eb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index c3fa8e11b..4db46f940 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -159,6 +159,14 @@ lemma cnv_fwd_flat (a) (h) (I) (G) (L):
 ] -H /2 width=1 by conj/
 qed-.
 
+lemma cnv_fwd_pair_sn (a) (h) (I) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![a,h] → ⦃G,L⦄ ⊢ V ![a,h].
+#a #h * [ #p ] #I #G #L #V #T #H
+[ elim (cnv_inv_bind … H) -H #HV #_
+| elim (cnv_fwd_flat … H) -H #HV #_
+] //
+qed-.
+
 (* Basic_2A1: removed theorems 3:
               shnv_cast shnv_inv_cast snv_shnv_cast
 *)