X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fterm.ma;h=b0fc86df39784d2b617d14228c26adc45628c734;hp=93cce0ffc42f2a142fddbf8217b4d215b68aa690;hb=a0b7db9844126ebcdf4b5dbb586514854cef5d93;hpb=31be09cc0d040577917783e050e1d38c0daa8f01

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
index 93cce0ffc..b0fc86df3 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
@@ -92,6 +92,13 @@ interpretation "native type annotation (term)"
 
 (* Basic properties *********************************************************)
 
+lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ{p}W.T
+                     | (∀p,W,T. X = ⓛ{p}W.T → ⊥).
+* [ #I | * [ #p * | #I ] #V #T ]
+[3: /3 width=4 by ex1_3_intro, or_introl/ ]
+@or_intror #q #W #U #H destruct
+qed-.
+
 (* Basic_1: was: term_dec *)
 lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2).
 #T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ]