HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  eqtypri GIF version

Definition eqtypri 71
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)
Hypotheses
Ref Expression
eqtypri.1 A:α
eqtypri.2 R⊧[B = A]
Assertion
Ref Expression
eqtypri B:α

Detailed syntax breakdown of Definition eqtypri
StepHypRef Expression
1 hal . 2 type α
2 tb . 2 term B
31, 2wffMMJ2t 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