定义上相等（Definitional Equality）指的是意义上相等，即同义，包括了，定义的缩写（Abbreviatory Definition），alpha转换，相同替代（substituting equals for equals）等。下面是LEAN给定的何谓 定义上相等。          注：罗列的推演规则中，如自明其义的，则不多加解析其前提、结果、或特定注解。