Nuprl Lemma : guard_functionality_wrt_iff

p,q:.  ({p  q}  {{p}  {q}})


Proof not projected



Definitions occuring in Statement :  prop: ,  guard: {T},  all: x:A. B[x],  iff: P  Q,  implies: P  Q
Definitions :  all: x:A. B[x],  prop: ,  implies: P  Q,  guard: {T},  iff: P  Q,  and: P  Q,  rev_implies: P  Q,  member: t  T,  uall: [x:A]. B[x]
Lemmas :  iff_wf
\mforall{}p,q:\mBbbP{}.    (\{p  \mLeftarrow{}{}\mRightarrow{}  q\}  {}\mRightarrow{}  \{\{p\}  \mLeftarrow{}{}\mRightarrow{}  \{q\}\})


Date html generated: 2011_10_20-PM-04_06_29
Last ObjectModification: 2011_09_28-PM-12_25_34

Home Index