Skip to content

remove mem_setT? #1885

@affeldt-aist

Description

@affeldt-aist

Lemma mem_setT (u : T) : u \in [set: T]. Proof. by rewrite inE. Qed.

It is the same as in_setT and is actually not used in the development.

Metadata

Metadata

Assignees

No one assigned

    Labels

    renaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions