X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Flfpr.ma;h=5e1ba79926c492ea5f353bb1e9270edaa30bfb58;hb=9c09a0b1f8801e40612eef429b82fc6dbae01b85;hp=c8adecd25dadefcfe2ab1bac99f799b7bba668ec;hpb=290c9eacc389bd57420f54e39354ed93142c8502;p=helm.git 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 c8adecd25..5e1ba7992 100644 --- 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.