Universe inconsistency `relation` and `list`
From stdpp Require Export fin_maps.
Definition foo A := list (relation A).
(* In environment
A : Type
The term "relation A" has type "Type@{max(Set+1,Coq.Relations.Relation_Definitions.1)}"
while it is expected to have type "Type@{list.u0}" (universe inconsistency: Cannot enforce
Coq.Relations.Relation_Definitions.1 <= list.u0 because list.u0 <= MapFold.u2
< Coq.Relations.Relation_Definitions.1).
*)
Reported by @andrew-appel, see https://mattermost.mpi-sws.org/iris/pl/4puh45xgoidktmcioxzec1tguo