Pred is the Conat destructor.
Added Stream-build.
Added doc.
Added doc: We couldn't prove Conat-coind.
Added doc: Agda doesn't accept the proof of Conat ∞.
s/_unf/_out.