X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fexamples%2Fex_fpbg_refl.ma;h=6ee55d8d0634d8c347c9f3b55e42a88a09fa5c34;hp=257015d95c14cd69dd8aaf7db31d9eadfe8b5cbe;hb=4173283e148199871d787c53c0301891deb90713;hpb=a67fc50ccfda64377e2c94c18c3a0d9265f651db

diff --git a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
index 257015d95..6ee55d8d0 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/examples/ex_fpbg_refl.ma
@@ -53,5 +53,5 @@ lemma fqup_ApplOmega_41 (G) (L) (s0) (s): ⦃G,L,ApplOmega4 s0 s⦄ ⊐+ ⦃G,L,
 
 (* Main properties **********************************************************)
 
-theorem fpbg_refl (h) (o) (G) (L) (s0) (s): ⦃G,L,ApplOmega1 s0 s⦄ >[h,o] ⦃G,L,ApplOmega1 s0 s⦄.
+theorem fpbg_refl (h) (G) (L) (s0) (s): ⦃G,L,ApplOmega1 s0 s⦄ >[h] ⦃G,L,ApplOmega1 s0 s⦄.
 /3 width=5 by fpbs_fpbg_trans, fqup_fpbg, cpxs_fpbs/ qed.