HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  eqtypi Structured version   Unicode version

Definition eqtypi 69
Description: Deduce equality of types from equality of expressions. (This is unnecessary but eliminates a lot of hypotheses.)
Hypotheses
Ref Expression
eqcomi.1 |- A:al
eqcomi.2 |- R |= [A = B]
Assertion
Ref Expression
eqtypi |- B:al

Detailed syntax breakdown of Definition eqtypi
StepHypRef Expression
1 hal . 2 type al
2 tb . 2 term B
31, 2wffMMJ2t 12 1 wff B:al
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