Higher-Order Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > HOLE Home > Th. List > eqtypi | GIF version |
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.) |
Ref | Expression |
---|---|
eqcomi.1 | ⊢ A:α |
eqcomi.2 | ⊢ R⊧[A = B] |
Ref | Expression |
---|---|
eqtypi | ⊢ 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: eqcomi 70 mpbi 72 ceq12 78 leq 81 eqtri 85 3eqtr4i 86 3eqtr3i 87 oveq123 88 hbxfrf 97 clf 105 cl 106 cla4ev 159 cbvf 167 cbv 168 leqf 169 ac 184 |
Copyright terms: Public domain | W3C validator |