---

{ b:
    [T:Type]
      A,B:T List. x:T.
        ((x  if b then A else B fi )
         ((b)  (x  A))  ((b)  (x  B))) }

{ Proof }

---

Definitions occuring in Statement :  assert: b,  ifthenelse: if b then t else f fi ,  bool: ,  uall: [x:A]. B[x],  all: x:A. B[x],  iff: P  Q,  not: A,  or: P  Q,  and: P  Q,  list: type List,  universe: Type,  l_member: (x  l)
Definitions :  all: x:A. B[x],  uall: [x:A]. B[x],  iff: P  Q,  ifthenelse: if b then t else f fi ,  or: P  Q,  and: P  Q,  assert: b,  not: A,  member: t  T,  implies: P  Q,  btrue: tt,  prop: ,  rev_implies: P  Q,  true: True,  false: False,  bfalse: ff,  guard: {T},  bool: ,  unit: Unit,  it:
Lemmas :  bool_wf,  iff_weakening_uiff,  assert_wf,  eqtt_to_assert,  not_wf,  uiff_transitivity,  bnot_wf,  eqff_to_assert,  assert_of_bnot,  false_wf

---

\mforall{}b:\mBbbB{}
    \mforall{}[T:Type]
        \mforall{}A,B:T  List.  \mforall{}x:T.    ((x  \mmember{}  if  b  then  A  else  B  fi  )  \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}b)  \mwedge{}  (x  \mmember{}  A))  \mvee{}  ((\mneg{}\muparrow{}b)  \mwedge{}  (x  \mmember{}  B)))


Date html generated: 2011_08_16-AM-11_10_42
Last ObjectModification: 2011_06_20-AM-00_18_50

Home Index