diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-12-04 13:57:57 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2013-12-04 13:58:18 +0100 |
commit | 12a55370b525185858aed77af4ef1dc0d5cf4e7e (patch) | |
tree | b262128ef711ac106d8e9d58e343b2280703f0d4 /theories/Logic/Eqdep_dec.v | |
parent | 3339c56fec1b9e9aab6f31c04ddbe3a77b5812ec (diff) |
Improved the presentation of the proof of UIP_refl_nat.
Diffstat (limited to 'theories/Logic/Eqdep_dec.v')
-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. |