X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flprs_ldrop.ma;h=f03d3f0e851fa42a8b79c7df6b04fb5a3982bb3b;hb=32bdf7f107be22a121fab8225c5fae4eb6b33633;hp=73c9281e65e8b2380dc72c8d4a0b5f9aca11e58b;hpb=e02bd4f3df78b5cc374d49d0ddf48b311188f514;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma
index 73c9281e6..f03d3f0e8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lprs_ldrop.ma
@@ -19,11 +19,11 @@ include "basic_2/computation/lprs.ma".
 
 (* Properies on local environment slicing ***********************************)
 
-lemma lprs_ldrop_conf: dropable_sn lprs.
+lemma lprs_ldrop_conf: ∀G. dropable_sn (lprs G).
 /3 width=3 by dropable_sn_TC, lpr_ldrop_conf/ qed-.
 
-lemma ldrop_lprs_trans: dedropable_sn lprs.
+lemma ldrop_lprs_trans: ∀G. dedropable_sn (lprs G).
 /3 width=3 by dedropable_sn_TC, ldrop_lpr_trans/ qed-.
 
-lemma lprs_ldrop_trans_O1: dropable_dx lprs.
+lemma lprs_ldrop_trans_O1: ∀G. dropable_dx (lprs G).
 /3 width=3 by dropable_dx_TC, lpr_ldrop_trans_O1/ qed-.