\documentclass[a4paper,leqno]{strayman}
+\errorcontextlines=50
\let\numberwithin=\notdef
\usepackage{amsmath}
\usepackage{mathabx}
\newif\ifhidehack\hidehackfalse
\DeclareRobustCommand\hidefromedef[2]{%
\hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
- \newcommand{\pa}[1]{\hidefromedef{\varmathbb #1}{#1}}
+ \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
-\newcommand{\set}[1]{\mathbb #1}
+\newcommand{\set}[1]{\mathbb{#1}}
\newcommand{\pay}[1]{\pa{#1}^+}
\newcommand{\pan}[1]{\pa{#1}^-}
$A \le C \equiv A \le L \lor A \le R \lor A = C$.
But $C \in py$ and $A \in \pn$ so $A \neq C$.
-Thus $A \le L \lor A \le R$.
+Thus $fixme this is not really the right thing A \le L \lor A \le R$.
By Unique Base of L and Transitive Ancestors,
$A \le L \equiv A \le \baseof{L}$.