milestone in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma
index 271094919b6cfc8f66d6b98786f4665364a4a4c9..9887fa77cc761c0431d4e1d60520db49343f621b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lpss.ma
@@ -89,4 +89,4 @@ elim (lpss_cpss_conf_dx … HU12 … HL12) -L1 #U #HU1 #HU2
 elim (cpss_conf … HU1 … HUT1) -U1 #U1 #HU1 #HTU1
 lapply (cpss_trans … HU2 … HU1) -U
 lapply (cprs_cpss_trans … HT21 … HTU1) -T1 /2 width=3/
-qed-.
\ No newline at end of file
+qed-.