- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / cpr_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
index 43bce2b1afe687b5f59355b001f1d9fc7948ed61..b54510e8cabf09946e140210f39160bffb8ee129 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma
@@ -134,7 +134,7 @@ elim (cpr_inv_appl1 … H) -H *
   elim (simple_inv_bind … HT1)
 ]
 qed-.
-
+     
 (* Relocation properties ****************************************************)
 
 (* Basic_1: was: pr2_lift *)