Decidability of equality (draft)

[helm.git] / matita / matita / lib / lambdaN / subterms.ma

diff --git a/matita/matita/lib/lambdaN/subterms.ma b/matita/matita/lib/lambdaN/subterms.ma
index 7773ddcf11926eab0223f61d257b5ce11aeb3410..86a8507ed55bb13590988bd76476056a3354f124 100644 (file)
--- 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 (?%).