]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/static_2/static/req_fsle.ma
some restyling ...
[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / req_fsle.ma
index d91c9905b96a5167d42a8cac456828325a07c232..efafbb90369a8f4f1ee1d426c165d163eb50da2e 100644 (file)
@@ -29,5 +29,5 @@ qed.
 (* Forward lemmas with free variables inclusion for restricted closures *****)
 
 lemma req_rex_trans: ∀R. req_transitive R →
-                     ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R, T] L2 → L1 ⪤[R, T] L2.
+                     ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤[R,T] L2 → L1 ⪤[R,T] L2.
 /4 width=16 by req_fsle_comp, rex_trans_fsle, rex_trans_next/ qed-.