X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fstatic%2Flfdeq_fqus.ma;h=f78c3e8eb3782706a97aaf1ae6bef899f65d531d;hp=9d4c4a67b1f9f8fb92dfbbd1bd80dd10700bd215;hb=b3afed9fd3cc38ecd4578f6b0741be50872a2828;hpb=268e7f336d036f77ffc9663358e9afda92b97730

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
index 9d4c4a67b..f78c3e8eb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
@@ -60,7 +60,7 @@ lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K
 #h #o #b #G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U
 [ #I #G #L2 #V2 #L1 #H elim (lfdeq_inv_zero_pair_dx … H) -H
   #K1 #V1 #HV1 #HV12 #H destruct
-  /3 width=7 by tdeq_lfdeq_conf_sn, fqu_lref_O, ex3_2_intro/
+  /3 width=7 by tdeq_lfdeq_conf, fqu_lref_O, ex3_2_intro/
 | * [ #p ] #I #G #L2 #V #T #L1 #H
   [ elim (lfdeq_inv_bind … H)
   | elim (lfdeq_inv_flat … H)
@@ -100,7 +100,7 @@ lemma lfdeq_fqup_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐+[b] ⦃G2,
   elim (lfdeq_fqu_trans … HU2 … HK0) -K #K1 #U1 #HU1 #HU12 #HK12
   elim (tdeq_fqu_trans … HU1 … HU0) -U #K3 #U3 #HU03 #HU31 #HK31
   @(ex3_2_intro … K3 U3) (**) (* full auto too slow *)
-  /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf_sn, fqup_strap1, tdeq_trans/
+  /3 width=5 by lfdeq_trans, tdeq_lfdeq_conf, fqup_strap1, tdeq_trans/
 ]
 qed-.