Mercurial > cpdt > repo

comparison src/MoreDep.v @ 335:1f57a8d0ed3d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Pass over Subset
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Oct 2011 11:32:13 -0400
parents d5787b70cf48
children c7faf3551c5d
comparison
equal deleted inserted replaced
334:386b7ad8849b 335:1f57a8d0ed3d
991 991
992 Lemma substring_suffix_emp : forall s n m, 992 Lemma substring_suffix_emp : forall s n m,
993 substring n m s = "" 993 substring n m s = ""
994 -> m > 0 994 -> m > 0
995 -> n >= length s. 995 -> n >= length s.
996 destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption]. 996 destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
997 Qed. 997 Qed.
998 998
999 Hint Rewrite substring_stack substring_stack' substring_suffix 999 Hint Rewrite substring_stack substring_stack' substring_suffix
1000 using omega : cpdt. 1000 using omega : cpdt.
1001 1001