X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freqx_reqx.ma;h=8f9999e64107a6d61d3f5e237e3072b5c2e2539c;hp=b6dc3d196b2cacee4373babb5767eca8164cac96;hb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;hpb=b118146b97959e6a6dde18fdd014b8e1e676a2d1

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
index b6dc3d196..8f9999e64 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/reqx_reqx.ma
@@ -24,7 +24,7 @@ lemma reqx_sym: ∀T. symmetric … (reqx T).
 *)
 (* Basic_2A1: uses: lleq_dec *)
 lemma reqx_dec: ∀L1,L2. ∀T:term. Decidable (L1 ≅[T] L2).
-/2 width=1 by reqg_dec/ qed-.
+/3 width=1 by reqg_dec, sfull_dec/ qed-.
 (*
 (* Main properties **********************************************************)