- lsubsx (replacement of lcosx) completed

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

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 ab52a91505b67f961d926ca9b238e75e3f5e760c..58cf547d618f8d93de8d264d22dd9825f92c8c51 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
@@ -32,7 +32,7 @@ lemma fqu_tdeq_conf: ∀h,o,b,G1,G2,L1,L2,U1,T1. ⦃G1, L1, U1⦄ ⊐[b] ⦃G2,
   /2 width=5 by fqu_pair_sn, ex3_2_intro/
 | #p #I #G #L #W1 #U1 #X #H
   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
-  /3 width=5 by lfdeq_pair, fqu_bind_dx, ex3_2_intro/
+  /3 width=5 by lfdeq_pair_refl, fqu_bind_dx, ex3_2_intro/
 | #p #I #G #L #W1 #U1 #Hb #X #H
   elim (tdeq_inv_pair1 … H) -H #W2 #U2 #HW12 #HU12 #H destruct
   /3 width=5 by fqu_clear, ex3_2_intro/
@@ -74,7 +74,7 @@ lemma lfdeq_fqu_trans: ∀h,o,b,G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐[b] ⦃G2, K
   /2 width=5 by fqu_flat_dx, ex3_2_intro/
 | #I #G #L2 #T #U #HTU #Y #HU
   elim (lfdeq_fwd_dx … HU) #L1 #V1 #H destruct
-  /5 width=12 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
+  /5 width=14 by lfdeq_inv_lifts_bi, fqu_drop, drops_refl, drops_drop, ex3_2_intro/
 ]
 qed-.