X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flfpxs_fqup.ma;h=6c7615ce4dec2c6060555a7e6ee79182017d8c34;hp=0f90e90e21377c2cd42fc92c6357069186ab38c0;hb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d;hpb=9d5724b7a571ce0da2a2691e639f044430f4a73a diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma index 0f90e90e2..6c7615ce4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -19,7 +19,6 @@ include "basic_2/rt_computation/lfpxs.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: uses: lpxs_refl *) lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T). /2 width=1 by tc_lfxs_refl/ qed.