milestone update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / reqx_reqx.ma

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 b6dc3d196b2cacee4373babb5767eca8164cac96..8f9999e64107a6d61d3f5e237e3072b5c2e2539c 100644 (file)
--- 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 **********************************************************)