proposition: Lemma inverse_per_single : forall A (a b:A), inverse (per_single a b) = per_single b a.
proof: Proof. Proof using. intros. applys pred_ext_2. intros. unfold inverse, per_single. autos*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)