---

{ [A:Type]. [eq:EqDecider(A)]. [x:A]. [v,P:Top].
    (z != x : v(x) ==> P[a;z] ~ True  P[x;v]) }

{ Proof }

---

Definitions occuring in Statement :  fpf-single: x : v,  fpf-val: z != f(x) ==> P[a; z],  uall: [x:A]. B[x],  top: Top,  so_apply: x[s1;s2],  implies: P  Q,  true: True,  universe: Type,  sqequal: s ~ t,  deq: EqDecider(T)
Definitions :  fpf-val: z != f(x) ==> P[a; z],  fpf-single: x : v,  fpf-dom: x  dom(f),  deq-member: deq-member(eq;x;L),  pi1: fst(t),  reduce: reduce(f;k;as),  member: t  T,  assert: b,  bor: p q,  btrue: tt,  ifthenelse: if b then t else f fi ,  implies: P  Q,  sq_type: SQType(T),  uall: [x:A]. B[x],  uimplies: b supposing a,  all: x:A. B[x],  guard: {T}
Lemmas :  subtype_base_sq,  bool_wf,  bool_subtype_base,  top_wf,  deq_wf,  eqof_eq_btrue,  btrue_wf

---

\mforall{}[A:Type].  \mforall{}[eq:EqDecider(A)].  \mforall{}[x:A].  \mforall{}[v,P:Top].    (z  !=  x  :  v(x)  ==>  P[a;z]  \msim{}  True  {}\mRightarrow{}  P[x;v])


Date html generated: 2011_08_10-AM-08_03_11
Last ObjectModification: 2011_06_18-AM-08_20_56

Home Index