From 052c5c2ca4c5257716ada059fbc723c975428a61 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 21 Jun 2011 20:35:04 +0000 Subject: [PATCH] missing ; to delimit syntax :( --- matita/matita/lib/basics/list.ma | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma index e4bdcb8aa..8b0449987 100644 --- a/matita/matita/lib/basics/list.ma +++ b/matita/matita/lib/basics/list.ma @@ -211,9 +211,8 @@ lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l. #A #n elim n -n // #n #IHn #l elim l normalize // 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. -*) \ No newline at end of file -- 2.39.2