Theorems for Congruent Morphisms

[sebasguts]

Example: If a category has a ZeroObject, MorphismFromZeroObject and MorphismFromInitialObject should compute congruent morphisms. If a theorem is installed for the later, a corresponding theorem should be installed for the first operation.