\documentclass[a4paper,leqno]{strayman}
+\errorcontextlines=50
\let\numberwithin=\notdef
\usepackage{amsmath}
\usepackage{mathabx}
$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}$.
But by Tip Merge condition on $\baseof{R}$,
$A \le \baseof{L} \implies A \le \baseof{R}$, so
-$A \le \baseof{R} \lor A \le \baseof{R} \equiv A \le \baseof{R}$.
+$A \le \baseof{R} \lor A \le \baseof{L} \equiv A \le \baseof{R}$.
Thus $A \le C \equiv A \le \baseof{R}$. Ie, $\baseof{C} =
\baseof{R}$.
+\subsubsection{For $R \in \pn$:}
+
UP TO HERE
By Tip Merge, $A \le $