partial commit: "computation" component ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / lprs_ldrop.ma

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 73c9281e65e8b2380dc72c8d4a0b5f9aca11e58b..f03d3f0e851fa42a8b79c7df6b04fb5a3982bb3b 100644 (file)
--- 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-.