$`\require{color} % 緑色
\newcommand{\In}{ \text{ in }}
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\For}{\Keyword{For } } % 使用
\newcommand{\Let}{\Keyword{Let } }% 使用
\newcommand{\When}{\Keyword{When } }% 使用
\newcommand{\And}{\Keyword{And } }%
\newcommand{\Holds}{\Keyword{Holds } }%
\newcommand{\HoldsI}{\Keyword{Holds! } }%
\newcommand{\HoldsQ}{\Keyword{Holds? } }% 使用
\newcommand{\BecauseOf}{\Keyword{Because Of } }%
\newcommand{\Fact }{\Keyword{Fact } }%
\newcommand{\Judgement }{\Keyword{Judgement } }%
\newcommand{\Question }{\Keyword{Question } }% 使用
\newcommand{\DeclFunction }{\Keyword{Decl Function } }%
\newcommand{\DefFunction }{\Keyword{Def Function } }%
\newcommand{\Given}{\Keyword{Given } }%
\newcommand{\Returns}{\Keyword{Returns } }%
\newcommand{\ReturnsI}{\Keyword{Returns! } }%
\newcommand{\ReturnsQ}{\Keyword{Returns? } }%
\newcommand{\Body}{\Keyword{Body } }%
\newcommand{\WeShouldKnow}{\Keyword{WeShouldKnow } }% 使用
`$
$`\WeShouldKnow \text{単射, 関数のグラフ集合, 関係の転置, 対角集合}\\
\WeShouldKnow \text{IsInjective}, \mrm{Graph}, (\_)^t, \Delta_X
`$
$`\Question \text{Q1}\\
\quad \For f:X \to Y \In{\bf Set}\\
\quad \When \text{IsInjective}(f) \\
\quad \Let F := \mrm{Graph}(f) \\
\HoldsQ F;F^t \subseteq \Delta_X
`$
$`\Question \text{Q2}\\
\quad \For f:X \to Y \In{\bf Set}\\
\quad \Let F := \mrm{Graph}(f) \\
\quad \When F;F^t \subseteq \Delta_X\\
\HoldsQ \text{IsInjective}(f)
`$
