X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Ffpbg.ma;h=ba56fd0c53f12f3b96552162e7c6816fbbad038f;hb=6b4da5fa47d474dcf2f203ec7f5ed36938739c9b;hp=1ce29c009e4859aae2dbc6fc90045f0975c0782f;hpb=bd840d43d09254b41936c49fc447e58582b156eb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
index 1ce29c009..ba56fd0c5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/fpbg.ma
@@ -38,6 +38,13 @@ lemma fpbg_fpbq_trans: ∀h,G1,G,G2,L1,L,L2,T1,T,T2.
 /3 width=9 by fpbs_strap1, ex2_3_intro/
 qed-.
 
+lemma fpbg_fqu_trans (h): ∀G1,G,G2,L1,L,L2,T1,T,T2.
+                          ⦃G1, L1, T1⦄ >[h] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐ ⦃G2, L2, T2⦄ →
+                          ⦃G1, L1, T1⦄ >[h] ⦃G2, L2, T2⦄.
+#h #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2
+/4 width=5 by fpbg_fpbq_trans, fpbq_fquq, fqu_fquq/
+qed-.
+
 (* Note: this is used in the closure proof *)
 lemma fpbg_fpbs_trans: ∀h,G,G2,L,L2,T,T2. ⦃G, L, T⦄ ≥[h] ⦃G2, L2, T2⦄ →
                        ∀G1,L1,T1. ⦃G1, L1, T1⦄ >[h] ⦃G, L, T⦄ → ⦃G1, L1, T1⦄ >[h] ⦃G2, L2, T2⦄.