- we introduced the pointer_step rc in the perspective of proving

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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
index c8adecd25dadefcfe2ab1bac99f799b7bba668ec..5e1ba79926c492ea5f353bb1e9270edaa30bfb58 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lfpr.ma
@@ -27,6 +27,7 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+(* Note: lemma 250 *)
 lemma lfpr_refl: ∀L. ⦃L⦄ ➡ ⦃L⦄.
 /2 width=3/ qed.