X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ffpbg.ma;h=0755ebf79960759c76b8d4312e356c9b17d042ef;hb=f282b35b958c9602fb1f47e5677b5805a046ac76;hp=b5c336e2474f9eb8ac35b470934526da2b3bf997;hpb=cb5ca7ea4e826e9331eabeaea44353caab00071e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
index b5c336e24..0755ebf79 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
@@ -40,7 +40,7 @@ lemma fpbg_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2.
 /2 width=5 by tri_TC_strap/ qed.
 
 (* Note: this is used in the closure proof *)
-lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+lemma fqup_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
 /4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed.
 
 (* Basic eliminators ********************************************************)