Removed a comment.
s/intro/intros.
Proved Conat_in.