- some theorems from levels_defs

[helm.git] / matita / contribs / LAMBDA-TYPES / Level-1 / problems.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
index c727f77db854e3449ae2463a6c46fa2ba497ed3e..9f9ce1b3642781a5fe80b321a609e92eaa7b65fe 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/problems.ma
@@ -22,6 +22,7 @@ include "LambdaDelta/theory.ma".
 
 (*  iso_trans (in problems-1)
  *  drop1_getl_trans (in problems-2)
+ *  asucc_inj (in problems-3)
  *)
 
 (* Problem 2: assertion failure raised by type checker on this object *)