X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_max.ma;h=cb902736e1de5bbc7c1c02d33a2a79d4fadc4fad;hp=44c3539b9eb0035c26509880827f14df182de90e;hb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;hpb=da0775e27b362e91ea1453a800bc403781cc2ca3 diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma index 44c3539b9..cb902736e 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma @@ -39,7 +39,7 @@ qed. (*** max_SS *) lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2). #n1 #n2 -@trans_eq [3: @ntri_succ_bi | skip ] (**) (* rewrite fails because δ-expansion gets in the way *) +@trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)