diff options
| -rw-r--r-- | theories/Init/Specif.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 4ff007570e..1fb6dabe6f 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -765,7 +765,7 @@ Section Dependent_choice_lemmas. exists f. split. - reflexivity. - - induction n; simpl; apply proj2_sig. + - intro n; induction n; simpl; apply proj2_sig. Defined. End Dependent_choice_lemmas. |