aboutsummaryrefslogtreecommitdiffstats
path: root/lib/Heaps.v
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Heaps.v')
-rw-r--r--lib/Heaps.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Heaps.v b/lib/Heaps.v
index 2a21f88c..9fa07a1d 100644
--- a/lib/Heaps.v
+++ b/lib/Heaps.v
@@ -432,7 +432,7 @@ Lemma lt_heap_In:
Proof.
induction h; simpl; intros.
contradiction.
- intuition. apply le_lt_trans with x0; auto. red. left. apply E.eq_sym; auto.
+ intuition. apply le_lt_trans with x0; auto. red. left. assumption.
Qed.
Lemma findMax_max: