X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpxs.ma;h=e13e044c327802523e73aa6282839a040cd6a4cc;hb=e2b4ff64df523b4be9d7dc4e92386945846426e7;hp=f09fab54c88ba805d37c73b6727ed6bb01173233;hpb=1330e8b45155fc972bc18c4e5fd69897afa3cbe8;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma index f09fab54c..e13e044c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs.ma @@ -144,3 +144,5 @@ elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3 by cpxs_strap1, or3_intro1, or3_int lapply (cpxs_strap1 … HW1 … HW2) -W lapply (cpxs_strap1 … HT1 … HT2) -T /3 width=5 by or3_intro0, ex3_2_intro/ qed-. + +(* Basic_2A1: removed theorems 1: cpxs_neq_inv_step_sn *)