Definition weq 38

Description: The equality function has type α → α → ∗, i.e. it is polymorphic over all types, but the left and right type must agree.

Assertion

Ref	Expression
weq	⊢ = :(α → (α → ∗))

Detailed syntax breakdown of Definition weq

Step	Hyp	Ref	Expression
1		hal	. . 3 type α
2		hb 3	. . . 4 type ∗
3	1, 2	ht 2	. . 3 type (α → ∗)
4	1, 3	ht 2	. 2 type (α → (α → ∗))
5		ke 7	. 2 term =
6	4, 5	wffMMJ2t 12	1 wff = :(α → (α → ∗))

This definition is referenced by:  wtru  40  eqcomx  47  weqi  68  eqcomi  70  mpbi  72  eqid  73  ded  74  ceq12  78  leq  81  beta  82  distrc  83  distrl  84  eqtri  85  oveq123  88  hbov  101  clf  105  ovl  107  alval  132  euval  134  imval  136  anval  138  eta  166  cbvf  167  leqf  169  ax10  200  axrep  207