diff options
Diffstat (limited to 'theories/Wellfounded/Transitive_Closure.v')
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 2d139504f3..49c2dd8602 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,6 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. + #[local] Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. |