-xxx up to here
-
-By Insertion Acyclic, $D \not\isin R^+$. xxx this is wrong
-By Tip Contents for $R^+$,
-$D \isin R^+ \equiv D \isin R^- \lor (D \in \pry \land ...)$
-but $D \in \py$ so $D \not\in \pry$. So $D \not\isin R^-$.
-By $\merge$, $D \isin C \equiv D \isin L$.
+By Exclusive Tip Contents for $R^+$ ($D \not\in \pry$ case)
+$D \isin R^+ \equiv D \isin R^-$.
+So by $\merge$, $D \isin C \equiv D \isin L$.