proposition: Lemma per_empty: forall A, per (@LibRelation.empty A).
proof: Proof. Proof using. unfold LibRelation.empty. constructor. unfold sym. eauto. unfold trans. eauto. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)