diff options
| -rw-r--r-- | theories/Lists/PolyList.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 0a6d05956f..40af3d16e0 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -240,7 +240,8 @@ Lemma In_dec : ((x,y:A){x=y}+{~x=y}) -> (a:A)(l:list){(In a l)}+{~(In a l)}. Proof. Induction l. Right; Apply in_nil. - Intros; Elim H0; Simpl; Elim (H a0 a); Auto. + Intros; Elim (H a0 a); Simpl; Auto. + Elim H0; Simpl; Auto. Right; Unfold not; Intros [Hc1 | Hc2]; Auto. Save. |