renaming in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / aaa_fqus.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
index 7905a6a9f6a10b8a654b4797d9f757422fa134c1..812bcc3656984c1fb38363dd1e635f01346f699b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
@@ -34,6 +34,7 @@ lemma aaa_fqu_conf: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄
   [ elim (aaa_inv_abbr … H)
   | elim (aaa_inv_abst … H)
   ] -H /2 width=2 by ex_intro/
+| #p #I #G #L #V #T #H destruct
 | * #G #L #V #T #X #H
   [ elim (aaa_inv_appl … H)
   | elim (aaa_inv_cast … H)