update in ground_2, static_2, basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
index 93cce0ffc42f2a142fddbf8217b4d215b68aa690..be1313b0762e9a4a89be3a2ab3a9c8fc8e87ddd3 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/xoa/ex_1_3.ma".
 include "static_2/notation/functions/item0_1.ma".
 include "static_2/notation/functions/snitem2_3.ma".
 include "static_2/notation/functions/snbind2_4.ma".
@@ -92,6 +93,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 ]