X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Flfpr_drops.ma;h=7c630638c2b3f61fbf70b9ced2673c03dd1e008f;hb=58ea181757dce19b875b2f5a224fe193b2263004;hp=7d23f3b0f8cf5e829d601db46e2c8012da168b1a;hpb=670ad7822d59e598a38d9037d482d3de188b170c;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
index 7d23f3b0f..7c630638c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma
@@ -20,14 +20,17 @@ include "basic_2/rt_transition/lfpr.ma".
 
 (* Properties with generic slicing for local environments *******************)
 
+(* Basic_2A1: uses: drop_lpr_trans *)
 lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G).
 /3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-.
 
 (* Inversion lemmas with generic slicing for local environments *************)
 
+(* Basic_2A1: uses: lpr_drop_conf *)
 lemma lfpr_drops_conf: ∀h,G. dropable_sn (cpm 0 h G).
 /2 width=5 by lfxs_dropable_sn/ qed-.
 
+(* Basic_2A1: uses: lpr_drop_trans_O1 *)
 lemma lfpr_drops_trans: ∀h,G. dropable_dx (cpm 0 h G).
 /2 width=5 by lfxs_dropable_dx/ qed-.