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

Theorem nvarjust 276
Description: A variable is equivalent to a nilad which always returns that variable.
Assertion
Ref Expression
nvarjust x = {r | [rx] 1}
Distinct variable group:   r,x

Proof of Theorem nvarjust
StepHypRef Expression
Colors of variables: wff var nilad
Syntax hints:  1wone 103  nvar 203  [wse 204   = weq 246  {nnab 266
 WARNING: This theorem has an incomplete proof.
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator