diff options
Diffstat (limited to 'theories/Sets/Partial_Order.v')
| -rwxr-xr-x | theories/Sets/Partial_Order.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 7b0f432ba..a1c1639f0 100755 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -87,6 +87,7 @@ Qed. Lemma Strict_Rel_Transitive: (Transitive U (Strict_Rel_of U D)). Red. Intros x y z H' H'0. -Apply Strict_Rel_Transitive_with_Rel with y := y; Intuition. +Apply Strict_Rel_Transitive_with_Rel with y := y; + [ Intuition | Unfold Strict_Rel_of in H' H'0; Intuition ]. Qed. End Partial_order_facts. |