instance List.instLawfulOrderOrd {α : Type u_1} [LE α] [LT α] [Ord α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Std.LawfulOrderOrd α] : Std.LawfulOrderOrd (List α)

@[instance_reducible]

instance List.instLinearOrderPackage {α : Type u_1} [LE α] [LT α] [Ord α] [h : BEq α] [DecidableEq α] [DecidableLT α] [Std.IsLinearOrder α] [Std.LawfulOrderLT α] [Std.LawfulOrderOrd α] [Std.LawfulOrderBEq α] : Std.LinearOrderPackage (List α)