X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fs_transition%2Ffqu.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fs_transition%2Ffqu.ma;h=0f5feb7fc88c4739f3f83d303138aa8500a120d7;hb=775106f04b47236bf47e4321d745ec360ab4ebb4;hp=8dcfa103d10e4bd0a8f9b529675039be8527c153;hpb=cafb43926d8553c5b7f8dafcb5d734783c19bbfb;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
index 8dcfa103d..0f5feb7fc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
@@ -44,7 +44,13 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma fqu_lref_S: ∀b,I,G,L,V,i. ⦃G, L.ⓑ{I}V, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄.
+lemma fqu_sort: ∀b,I,G,L,s. ⦃G, L.ⓘ{I}, ⋆s⦄ ⊐[b] ⦃G, L, ⋆s⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_lref_S: ∀b,I,G,L,i. ⦃G, L.ⓘ{I}, #⫯i⦄ ⊐[b] ⦃G, L, #i⦄.
+/2 width=1 by fqu_drop/ qed.
+
+lemma fqu_gref: ∀b,I,G,L,l. ⦃G, L.ⓘ{I}, §l⦄ ⊐[b] ⦃G, L, §l⦄.
 /2 width=1 by fqu_drop/ qed.
 
 (* Basic inversion lemmas ***************************************************)