X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fetc_new%2Flreq%2Flreq_lreq.etc;h=3cb7451ec84f64d964bebf1dab7575fa486bef9d;hb=9b8d36ee041582f876543086e7659ed9e365e861;hp=20d6c0002903f7fe8f0e31409611e06e9e2d83cf;hpb=2c8220e5e0c09486355aa79d5cd8a7716c444aca;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc
index 20d6c0002..3cb7451ec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc
@@ -19,8 +19,8 @@ include "basic_2/grammar/lreq.ma".
 
 (* Main properties **********************************************************)
 
-theorem lreq_trans: ∀l,m. Transitive … (lreq l m).
-#l #m #L1 #L2 #H elim H -L1 -L2 -l -m
+theorem lreq_trans: ∀f. Transitive … (lreq f).
+#f #L1 #L2 #H elim H -L1 -L2 -l -m
 [ #l #m #X #H lapply (lreq_inv_atom1 … H) -H
   #H destruct //
 | #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H