X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Flsubc_lsuba.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fcomputation%2Flsubc_lsuba.ma;h=41c906285f3790160e5823642b99ab3a2f764288;hb=30f9071732ef8d6957deac4179f39799eddda267;hp=0000000000000000000000000000000000000000;hpb=d833e40ce45e301a01ddd9ea66c29fb2b34bb685;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma
new file mode 100644
index 000000000..41c906285
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/static/lsuba.ma".
+include "Basic_2/computation/acp_aaa.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* properties concerning lenv refinement for atomic arity assignment ********)
+
+lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+                   ∀L1,L2. L1 ÷⊑ L2 → L1 [RP] ⊑ L2.
+#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
+// /2 width=1/ /3 width=4/
+qed.