X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Faaa.ma;h=b5f416344d5545ec866769b316e77ac0a9fae805;hb=bdff98417627c404aacec8ebb07812287783c500;hp=7b4813491846a0fcd3b7ebfc335bbc37e0cee1cf;hpb=380ceb6b6552fd9ebd48d710ab12931d5d97e465;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..b5f416344 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
@@ -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