Theorem and_congr

Modification history