Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c. Proof.
Fail congruence. intros.
congruence with ((Triple a a a)) ((Triple d c a)). Qed.
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.