diff options
Diffstat (limited to 'theories/Structures')
| -rw-r--r-- | theories/Structures/OrderedType.v | 4 | ||||
| -rw-r--r-- | theories/Structures/OrdersLists.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index beb10a833..f84cdf32c 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -223,7 +223,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. @@ -396,7 +396,7 @@ Module KeyOrderedType(O:OrderedType). Qed. Lemma Inf_eq : forall l x x', eqk x x' -> Inf x' l -> Inf x l. - Proof. exact (InfA_eqA eqk_equiv ltk_compat). Qed. + Proof. exact (InfA_eqA eqk_equiv ltk_strorder ltk_compat). Qed. Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 059992f5b..f83b63779 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -32,7 +32,7 @@ Lemma Inf_lt : forall l x y, lt x y -> Inf y l -> Inf x l. Proof. exact (InfA_ltA lt_strorder). Qed. Lemma Inf_eq : forall l x y, eq x y -> Inf y l -> Inf x l. -Proof. exact (InfA_eqA eq_equiv lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv lt_strorder lt_compat). Qed. Lemma Sort_Inf_In : forall l x a, Sort l -> Inf a l -> In x l -> lt a x. Proof. exact (SortA_InfA_InA eq_equiv lt_strorder lt_compat). Qed. |