---

{ [A:Type]. [d1,d2,d3,d4:EqDecider(A)]. [B:A  Type]. [f,g:a:A fp-> B[a]].
  [x:A]. [z:B[x]].
    (f(x)?z = g(x)?z) supposing ((x  dom(f)) and f  g) }

{ Proof }

---

Definitions occuring in Statement :  fpf-sub: f  g,  fpf-cap: f(x)?z,  fpf-dom: x  dom(f),  fpf: a:A fp-> B[a],  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  so_apply: x[s],  function: x:A  B[x],  universe: Type,  equal: s = t,  deq: EqDecider(T)
Definitions :  not: A,  implies: P  Q,  false: False
Lemmas :  fpf-ap_functionality,  false_wf,  true_wf,  fpf-dom_functionality2,  assert_of_bnot,  eqff_to_assert,  uiff_transitivity,  bool_wf,  not_wf,  iff_weakening_uiff,  eqtt_to_assert,  ifthenelse_wf,  fpf-ap_wf,  subtype_rel_wf,  bnot_wf,  deq_wf,  fpf-sub_wf,  assert_wf,  fpf-dom_wf,  l_member_wf,  top_wf,  fpf_wf,  member_wf,  fpf-trivial-subtype-top,  fpf-cap_wf

---

\mforall{}[A:Type].  \mforall{}[d1,d2,d3,d4:EqDecider(A)].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f,g:a:A  fp->  B[a]].  \mforall{}[x:A].  \mforall{}[z:B[x]].
    (f(x)?z  =  g(x)?z)  supposing  ((\muparrow{}x  \mmember{}  dom(f))  and  f  \msubseteq{}  g)


Date html generated: 2011_08_10-AM-07_57_59
Last ObjectModification: 2011_06_18-AM-08_18_04

Home Index