\import{set.tex}

\subsection{Additional results about cons}

\begin{proposition}\label{cons_subseteq_intro}
    Suppose $x\in X$.
    Suppose $Y\subseteq X$.
    Then $\cons{x}{Y}\subseteq X$.
\end{proposition}

\begin{proposition}\label{cons_subseteq_elim}
    Suppose $\cons{x}{Y}\subseteq X$.
    Then $x\in X$ and $Y\subseteq X$.
\end{proposition}

\begin{proposition}\label{cons_subseteq_iff}
    $\cons{x}{Y}\subseteq X$ iff $x\in X$ and $Y\subseteq X$.
\end{proposition}

\begin{proposition}\label{subseteq_cons_right}
    If $C\subseteq B$, then $C\subseteq \cons{a}{B}$.
\end{proposition}

\begin{corollary}\label{subseteq_cons_self}
    $X\subseteq \cons{y}{X}$.
\end{corollary}

\begin{abbreviation}\label{remove_point}
    $\remove{a}{B} = B\setminus\{a\}$.
\end{abbreviation}

\begin{proposition}\label{subseteq_cons_intro_left}
    Suppose $a\in C \land \remove{a}{C} \subseteq B$.
    Then $C\subseteq \cons{a}{B}$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_cons,setminus_eq_emptyset_iff_subseteq}.
\end{proof}

\begin{proposition}\label{subseteq_cons_intro_right}
    Suppose $C \subseteq B$.
    Then $C\subseteq \cons{a}{B}$.
\end{proposition}

\begin{proposition}\label{subseteq_cons_elim}
    Suppose $C\subseteq \cons{a}{B}$.
    Then $C\subseteq B \lor (a\in C \land \remove{a}{C} \subseteq B)$.
\end{proposition}
\begin{proof}
    Follows by \cref{setminus_cons,subseteq,cons_iff,setminus_eq_emptyset_iff_subseteq}.
\end{proof}

\begin{proposition}\label{subseteq_cons_iff}
    $C\subseteq \cons{a}{B}$ iff $C\subseteq B \lor (a\in C \land \remove{a}{C}\subseteq B)$.
\end{proposition}


\begin{proposition}\label{remove_point_eq_setminus_singleton}
    $\remove{a}{B} = B\setminus\{a\}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}


\begin{proposition}\label{union_eq_cons}
    $\{a\}\union B = \cons{a}{B}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{cons_comm}
    $\cons{a}{\cons{b}{C}} = \cons{b}{\cons{a}{C}}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{cons_absorb}
    Suppose $a\in A$.
    Then $\cons{a}{A} = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{cons_remove}
    Suppose $a\in A$.
    Then $\cons{a}{A\setminus\{a\}} = A$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{cons_idempotent}
    Then $\cons{a}{\cons{a}{B}} = \cons{a}{B}$.
\end{proposition}
\begin{proof}
    Follows by set extensionality.
\end{proof}

\begin{proposition}\label{inters_cons}
    Suppose $B$ is inhabited.
    Then $\inters{\cons{a}{B}} = a\inter\inters{B}$.
\end{proposition}
\begin{proof}
    $\cons{a}{B}$ is inhabited.
    Thus for all $c$ we have $c\in\inters{\cons{a}{B}}$ iff $c\in a\inter \inters{B}$
        by \cref{inters_iff_forall,cons_iff,inter}.
    Follows by \hyperref[setext]{extensionality}.
\end{proof}