X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2FlambdaN%2Fsubterms.ma;h=86a8507ed55bb13590988bd76476056a3354f124;hb=d5d5925101dd773efb2f90136adc5d714a530cb9;hp=7773ddcf11926eab0223f61d257b5ce11aeb3410;hpb=c43cb5733fa62a81bf07e290729a450cbe24cee8;p=helm.git

diff --git a/matita/matita/lib/lambdaN/subterms.ma b/matita/matita/lib/lambdaN/subterms.ma
index 7773ddcf1..86a8507ed 100644
--- a/matita/matita/lib/lambdaN/subterms.ma
+++ b/matita/matita/lib/lambdaN/subterms.ma
@@ -19,7 +19,7 @@ inductive subterm : T → T → Prop ≝
   | prodl : ∀M,N. subterm M (Prod M N)
   | prodr : ∀M,N. subterm N (Prod M N)
   | dl : ∀M,N. subterm M (D M N)
-  | dr : ∀M,N. subterm M (D M N)
+  | dr : ∀M,N. subterm N (D M N)
   | sub_trans : ∀M,N,P. subterm M N → subterm N P → subterm M P.
 
 inverter subterm_myinv for subterm (?%).