  This note formally defines the concept of coinductive validity of judgements,
and contrasts it with inductive validity. For both notions it shows how a
judgement is valid iff it has a formal proof. Finally, it defines and
illustrates the notion of a proof by coinduction.
