partial commit in the relocation component to move some files ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / lreq / lreq_lreq.etc

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 20d6c0002903f7fe8f0e31409611e06e9e2d83cf..3cb7451ec84f64d964bebf1dab7575fa486bef9d 100644 (file)
--- 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