df-ii - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > df-ii		Structured version

Definition df-ii 292

Description: Definition of the I combinator.

**Assertion**
Ref	Expression
df-ii	⊦ I = λaa

**Detailed syntax breakdown of Definition df-ii**
Step	Hyp	Ref	Expression
1		nii 288	. 2 nilad I
2		va	. . 3 var a
3	2	nvar 203	. . 3 nilad a
4	2, 3	nla 279	. 2 nilad λaa
5	1, 4	weq 246	1 wff I = λaa

Colors of variables: wff var nilad

This definition is referenced by: (None)