the refactoring continues ...

[helm.git] / matita / matita / lib / basics / list.ma

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index 21dd7e3d1aa57597da06b06b7ba2c1c192b84be2..8b04499872f8ee473b9305d3f40fca4311d52d26 100644 (file)
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -214,5 +214,5 @@ qed.
 
 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 #A #n elim n -n /2/
-#n #IHn * normalize /2/
+#n #IHn *; normalize /2/
 qed.