Definition df-tru 299

Description: Church-encoding of truth. It takes two (curried) arguments and returns the first. Happens to be identical to nkk 287.

Assertion

Ref	Expression
df-tru	⊦ True = λxλyx

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-tru

Step	Hyp	Ref	Expression
1		ntru 297	. 2 nilad True
2		vx	. . 3 var x
3		vy	. . . 4 var y
4	2	nvar 203	. . . 4 nilad x
5	3, 4	nla 279	. . 3 nilad λyx
6	2, 5	nla 279	. 2 nilad λxλyx
7	1, 6	weq 246	1 wff True = λxλyx

This definition is referenced by: (None)