proposition: Lemma in_set_st_eq : forall (P:A->Prop) x, x \in set_st P = P x.
proof: Proof. Proof using. intros. apply* prop_ext. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)