Nuprl Lemma : squash_false

uiff(↓False;False)


Proof




Definitions occuring in Statement :  uiff: uiff(P;Q) squash: T false: False
Definitions unfolded in proof :  uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a member: t ∈ T false: False squash: T prop: uall: [x:A]. B[x]
Lemmas referenced :  false_wf squash_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalHypSubstitution imageElimination voidElimination hypothesis sqequalRule lemma_by_obid isectElimination thin imageMemberEquality hypothesisEquality baseClosed

Latex:
uiff(\mdownarrow{}False;False)



Date html generated: 2016_05_13-PM-03_13_37
Last ObjectModification: 2016_01_06-PM-05_49_21

Theory : core_2


Home Index