- degree assignment, static type assignment, iterated static type

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / lpr_lpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index b3e872e407be30b2d6a979bcaa4809033ec2c5f9..5d4c4707289c7e88defaf1b53697844199c92a8a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpr_ldrop.ma". (**) (* disambiguation error *)
 include "basic_2/grammar/lpx_sn_lpx_sn.ma".
 include "basic_2/substitution/fsupp.ma".
+include "basic_2/reduction/lpr_ldrop.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
 
@@ -126,7 +126,7 @@ fact cpr_conf_lpr_zeta_zeta:
 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 // /2 width=1/ -L0 -T0 #T #HT1 #HT2
 elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1/ #T1 #HT1 #HXT1
-elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2 
+elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1/ #T2 #HT2 #HXT2
 lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3/
 qed-.
 
@@ -228,7 +228,7 @@ elim (cpr_inv_abbr1 … H) -H *
   elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
   elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1 /2 width=1/ #Y #HYT #HXY
   @(ex2_intro … (ⓐV.Y)) /2 width=1/ /3 width=5/ (**) (* auto /4 width=9/ is too slow *)
-] 
+]
 qed-.
 
 fact cpr_conf_lpr_beta_beta: