X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Faarity.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Faarity.ma;h=db382096447ab7046a07a5e963bb64ab3cd9127c;hb=db020b4218272e2e35641ce3bc3b0a9b3afda899;hp=89199fabb3ea2b76f06b12b60fe976afeabb4409;hpb=d8f6494f48aa08bb32d9d1ac82fc16e9e41b76ac;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
index 89199fabb..db3820964 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/aarity.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-.