ground_2 released and permanently renamed as ground

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / aarity.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
index 89199fabb3ea2b76f06b12b60fe976afeabb4409..7a31b8c792bc497fa60d3b35d20e9741f5b0f1b3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
@@ -16,7 +16,7 @@
  * Initial invocation: - Patience on me to gain peace and perfection! -
  *)
 
-include "ground_2/lib/relations.ma".
+include "ground/lib/relations.ma".
 include "static_2/notation/functions/item0_0.ma".
 include "static_2/notation/functions/snitem2_2.ma".
 
@@ -72,3 +72,11 @@ lemma eq_aarity_dec: ∀A1,A2:aarity. Decidable (A1 = A2).
   ]
 ]
 qed-.
+
+lemma is_apear_dec (B) (X): Decidable (∃A. ②B.A = X).
+#B * [| #X #A ]
+[| elim (eq_aarity_dec X B) #HX ]
+[| /3 width=2 by ex_intro, or_introl/ ]
+@or_intror * #A #H destruct
+/2 width=1 by/
+qed-.