diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-02-25 13:53:49 -0500 |
|---|---|---|
| committer |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:41:53 -0400 |
| commit | 4c0079b2a5510abf8a5a4fc505c207383953c4cd (patch) | |
| tree | 493272f85eb39b4cbaefb8c698cb2381bda137a4 /coqprime | |
| parent | 6a38e9b00458f1dd7d51ec747c73c53a5c258b64 (diff) | |
Automate a UList proof a bit so it builds with 8.5
It still builds with 8.4
Diffstat (limited to 'coqprime')
| -rw-r--r-- | coqprime/Coqprime/UList.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/coqprime/Coqprime/UList.v b/coqprime/Coqprime/UList.v index 0b095cf94..32ca6b2a0 100644 --- a/coqprime/Coqprime/UList.v +++ b/coqprime/Coqprime/UList.v @@ -52,11 +52,9 @@ Qed. Theorem ulist_app_inv: forall l1 l2 (a : A), ulist (l1 ++ l2) -> In a l1 -> In a l2 -> False. intros l1; elim l1; simpl; auto. -intros a l H l2 a0 H0 [H1|H1] H2. -inversion H0 as [|a1 l0 H3 H4 H5]; auto. -case H4; rewrite H1; auto with datatypes. -apply (H l2 a0); auto. -apply ulist_inv with ( 1 := H0 ); auto. +intros a l H l2 a0 H0 [H1|H1] H2; +inversion H0 as [|a1 l0 H3 H4 H5]; clear H0; auto; + subst; eauto using ulist_inv with datatypes. Qed. (* Iinversion theorem the appended list *) |