Definition df-fal 300

Description: Church-encoding of falsity. It takes two (curried) arguments and returns the second.

Assertion

Ref	Expression
df-fal	⊦ False = λxλyy

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-fal

Step	Hyp	Ref	Expression
1		nfal 298	. 2 nilad False
2		vx	. . 3 var x
3		vy	. . . 4 var y
4	3	nvar 203	. . . 4 nilad y
5	3, 4	nla 279	. . 3 nilad λyy
6	2, 5	nla 279	. 2 nilad λxλyy
7	1, 6	weq 246	1 wff False = λxλyy

This definition is referenced by: (None)