Nuprl Lemma : dM-to-FL-sq
∀[I,J,v:Top].  (dM-to-FL(I;v) ~ dM-to-FL(J;v))
Proof
Definitions occuring in Statement : 
dM-to-FL: dM-to-FL(I;z)
, 
uall: ∀[x:A]. B[x]
, 
top: Top
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
dM-to-FL: dM-to-FL(I;z)
, 
lattice-extend: lattice-extend(L;eq;eqL;f;ac)
, 
lattice-fset-join: \/(s)
, 
lattice-0: 0
, 
lattice-join: a ∨ b
, 
union-deq: union-deq(A;B;a;b)
, 
lattice-fset-meet: /\(s)
, 
lattice-meet: a ∧ b
, 
face_lattice: face_lattice(I)
, 
face-lattice: face-lattice(T;eq)
, 
free-dist-lattice-with-constraints: free-dist-lattice-with-constraints(T;eq;x.Cs[x])
, 
constrained-antichain-lattice: constrained-antichain-lattice(T;eq;P)
, 
mk-bounded-distributive-lattice: mk-bounded-distributive-lattice, 
mk-bounded-lattice: mk-bounded-lattice(T;m;j;z;o)
, 
all: ∀x:A. B[x]
, 
top: Top
, 
eq_atom: x =a y
, 
ifthenelse: if b then t else f fi 
, 
bfalse: ff
, 
btrue: tt
, 
lattice-1: 1
Lemmas referenced : 
rec_select_update_lemma, 
top_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
sqequalRule, 
hypothesis, 
sqequalAxiom, 
lemma_by_obid, 
sqequalHypSubstitution, 
isect_memberEquality, 
isectElimination, 
thin, 
hypothesisEquality, 
because_Cache, 
dependent_functionElimination, 
voidElimination, 
voidEquality
Latex:
\mforall{}[I,J,v:Top].    (dM-to-FL(I;v)  \msim{}  dM-to-FL(J;v))
Date html generated:
2016_05_18-PM-00_11_54
Last ObjectModification:
2016_03_26-PM-08_35_05
Theory : cubical!type!theory
Home
Index