diff options
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/Eqdep_dec.v | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 9bde2d641..8979421da 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -358,17 +358,12 @@ Proof. end x). destruct x; reflexivity. - specialize IHn with (f_equal pred x). - change eq_refl with - (match (@eq_refl _ n) in _ = n' return S n = S n' with - | eq_refl => eq_refl - end). + change eq_refl with (f_equal S (@eq_refl _ n)). rewrite <- IHn; clear IHn. change (match S n as n' return S n = n' -> Prop with | 0 => fun _ => True | S n' => fun x => - x = match f_equal pred x in _ = n' return S n = S n' with - | eq_refl => eq_refl - end + x = f_equal S (f_equal pred x) end x). pattern (S n) at 2 3, x. destruct x; reflexivity. |