From 9c129000ea8bce2c794af6179524f42d88a330a1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 25 Feb 2016 13:53:49 -0500 Subject: Automate a UList proof a bit so it builds with 8.5 It still builds with 8.4 --- coqprime/Coqprime/UList.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) (limited to 'coqprime') 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 *) -- cgit v1.2.3