X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flist.ma;h=8b04499872f8ee473b9305d3f40fca4311d52d26;hb=fefe8d334012230f8e8b9d90976d9411a58d4ba8;hp=21dd7e3d1aa57597da06b06b7ba2c1c192b84be2;hpb=a6602de6db0993a67c5b23aedb3c8fe1d484855f;p=helm.git diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma index 21dd7e3d1..8b0449987 100644 --- 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.