\begin{proposition}\label{in_irrefl}
    For all sets $A$ we have $A\not\in A$.
\end{proposition}
\begin{proof}[Proof by \in-induction]
    %Let $B$ be a set.
    %Suppose $b\notin b$ for all $b\in B$.
    %Suppose $B\in B$.
    %But then
    %    $B\notin B$.
    Straightforward.
\end{proof}