X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Faaa.ma;h=f9a98fec1774767218ef95d981c0100fe619c9c9;hb=7abd5e0412171f7d07e085d334198c034895c2c3;hp=7b4813491846a0fcd3b7ebfc335bbc37e0cee1cf;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
index 7b4813491..f9a98fec1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -18,7 +18,7 @@ include "basic_2/substitution/ldrop.ma".
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
 inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) ⓪
+| aaa_sort: ∀L,k. aaa L (⋆k) (⓪)
 | aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
 | aaa_abbr: ∀a,L,V,T,B,A.
             aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A
@@ -63,6 +63,20 @@ lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ⁝ A →
                     ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
 /2 width=3/ qed-.
 
+fact aaa_inv_gref_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀p. T = §p → ⊥.
+#L #T #A * -L -T -A
+[ #L #k #q #H destruct
+| #I #L #K #V #B #i #HLK #HB #q #H destruct
+| #a #L #V #T #B #A #_ #_ #q #H destruct
+| #a #L #V #T #B #A #_ #_ #q #H destruct
+| #L #V #T #B #A #_ #_ #q #H destruct
+| #L #V #T #A #_ #_ #q #H destruct
+]
+qed.
+
+lemma aaa_inv_gref: ∀L,A,p. L ⊢ §p ⁝ A → ⊥.
+/2 width=6/ qed-.
+
 fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
                        ∃∃B. L ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A.
 #L #T #A * -L -T -A