set g = the ConwayGame;
take <* the ConwayGame*> ; :: thesis: <* the ConwayGame*> is ConwayGameChain-like
thus <* the ConwayGame*> is ConwayGameChain-like ; :: thesis: verum