Nuprl Lemma : int-decr-map-fun

[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k:ℤ]. ∀[v1,v2:Value].
  (v1 v2 ∈ Value) supposing ((<k, v1> ∈ m) and (<k, v2> ∈ m))


Definitions occuring in Statement :  int-decr-map-type: int-decr-map-type(Value) l_member: (x ∈ l) uimplies: supposing a uall: [x:A]. B[x] pair: <a, b> product: x:A × B[x] int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a l_member: (x ∈ l) int-decr-map-type: int-decr-map-type(Value) exists: x:A. B[x] cand: c∧ B all: x:A. B[x] nat: decidable: Dec(P) or: P ∨ Q pi2: snd(t) squash: T and: P ∧ Q prop: gt: i > j ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) false: False implies:  Q not: ¬A top: Top so_lambda: λ2x.t[x] so_apply: x[s] pi1: fst(t) so_apply: x[s1;s2] int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than: a < b subtype_rel: A ⊆B

\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v1,v2:Value].
    (v1  =  v2)  supposing  ((<k,  v1>  \mmember{}  m)  and  (<k,  v2>  \mmember{}  m))

Date html generated: 2016_05_17-PM-01_47_50
Last ObjectModification: 2016_01_17-AM-11_37_01

Theory : datatype-signatures

Home Index