X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Freq.ma;h=46e436d68eb2edde629e4b9d9659a114055b377f;hp=13965b92d796f8f83a13d62dc4c62976babe9cc9;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/req.ma b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
index 13965b92d..46e436d68 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/req.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/req.ma
@@ -69,7 +69,7 @@ lemma req_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#↑i] K2.ⓘ{I2} →
 (* Basic_2A1: was: llpx_sn_lrefl *)
 (* Basic_2A1: this should have been lleq_fwd_llpx_sn *)
 lemma req_fwd_rex: ∀R. c_reflexive … R →
-                   ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R, T] L2.
+                   ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤[R,T] L2.
 #R #HR #L1 #L2 #T * #f #Hf #HL12
 /4 width=7 by sex_co, cext2_co, ex2_intro/
 qed-.