diff options
Diffstat (limited to 'theories/Structures/OrdersLists.v')
| -rw-r--r-- | theories/Structures/OrdersLists.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index f83b6377..059992f5 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_strorder lt_compat). Qed. +Proof. exact (InfA_eqA eq_equiv 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. |