|
REFL |
reflexivity of equality |
|
TRANS |
transitivity of equality |
|
MK_COMB |
congruence of equality |
|
ABS |
abstraction of equality ( must not be free in ) |
|
BETA |
connection of abstraction and function application |
|
ASSUME |
assuming , prove |
|
EQ_MP |
relation of equality and deduction |
|
DEDUCT_ANTISYM_RULE |
deduce equality from 2-way deducibility |
|
INST |
instantiate variables in assumptions and conclusion of theorem |
|
INST_TYPE |
instantiate type variables in assumptions and conclusion of theorem |