Nuprl Lemma : dM1-sq-singleton-empty

[I:Top]. (1 {{}})


Proof




Definitions occuring in Statement :  dM1: 1 empty-fset: {} fset-singleton: {x} uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T dM1: 1 lattice-1: 1 record-select: r.x dM: dM(I) free-DeMorgan-algebra: free-DeMorgan-algebra(T;eq) mk-DeMorgan-algebra: mk-DeMorgan-algebra(L;n) record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff free-DeMorgan-lattice: free-DeMorgan-lattice(T;eq) free-dist-lattice: free-dist-lattice(T; eq) mk-bounded-distributive-lattice: mk-bounded-distributive-lattice mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o) btrue: tt fset-singleton: {x} cons: [a b] empty-fset: {} nil: [] it:
Lemmas referenced :  top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule hypothesis sqequalAxiom lemma_by_obid

Latex:
\mforall{}[I:Top].  (1  \msim{}  \{\{\}\})



Date html generated: 2016_05_18-AM-11_56_52
Last ObjectModification: 2016_02_04-PM-00_37_54

Theory : cubical!type!theory


Home Index