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

Theorem weq 41
Description: The equality function has type αα → ∗, i.e. it is polymorphic over all types, but the left and right type must agree. (Contributed by Mario Carneiro, 7-Oct-2014.)
Assertion
Ref Expression
weq = :(α → (α → ∗))

Proof of Theorem weq
StepHypRef Expression
1 ax-weq 40 1 = :(α → (α → ∗))
Colors of variables: type var term
Syntax hints:  ht 2  hb 3   = ke 7  wffMMJ2t 12
This theorem was proved from axioms:  ax-weq 40
This theorem is referenced by:  wtru  43  eqcomx  52  weqi  76  eqcomi  79  mpbi  82  eqid  83  ded  84  ceq12  88  leq  91  beta  92  distrc  93  distrl  94  eqtri  95  oveq123  98  hbov  111  clf  115  ovl  117  alval  142  euval  144  imval  146  anval  148  eta  178  cbvf  179  leqf  181  ax10  213  axrep  220
  Copyright terms: Public domain W3C validator