- the relation for pointwise extensions now takes a binder as argument

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / fpbg.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
index b5c336e2474f9eb8ac35b470934526da2b3bf997..0755ebf79960759c76b8d4312e356c9b17d042ef 100644 (file)
--- 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: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
+lemma fqup_fpbg: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >⋕[h, g] ⦃G2, L2, T2⦄.
 /4 width=1 by fpbc_fpbg, fpbu_fpbc, fpbu_fqup/ qed.
 
 (* Basic eliminators ********************************************************)