Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > eqtypri | GIF version |
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) |
Ref | Expression |
---|---|
eqtypri.1 | ⊢ A:α |
eqtypri.2 | ⊢ R⊧[B = A] |
Ref | Expression |
---|---|
eqtypri | ⊢ B:α |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hal | . 2 type α | |
2 | tb | . 2 term B | |
3 | 1, 2 | wffMMJ2t 12 | 1 wff B:α |
Colors of variables: type var term |
This definition is referenced by: mpbir 77 3eqtr4i 86 hbc 100 wal 124 wfal 125 wan 126 wim 127 wnot 128 wex 129 wor 130 weu 131 |
Copyright terms: Public domain | W3C validator |