diff options
Diffstat (limited to 'theories/Logic/FinFun.v')
| -rw-r--r-- | theories/Logic/FinFun.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/FinFun.v b/theories/Logic/FinFun.v index 2f72f16dea..086efb9841 100644 --- a/theories/Logic/FinFun.v +++ b/theories/Logic/FinFun.v @@ -216,7 +216,7 @@ Lemma Fin_Finite n : Finite (Fin.t n). Proof. induction n. - exists nil. - inversion a. + red;inversion a. - destruct IHn as (l,Hl). exists (Fin.F1 :: map Fin.FS l). intros a. revert n a l Hl. |