---

{ [x,L:Top].
    (rec-case(L) of
     [] => ff
     a::_ =>
      r.if a=2 x
         then tt
         else r ~ deq-member(IdDeq;x;L)) }

{ Proof }

---

Definitions occuring in Statement :  id-deq: IdDeq,  bfalse: ff,  btrue: tt,  uall: [x:A]. B[x],  top: Top,  list_ind: list_ind def,  sqequal: s ~ t,  deq-member: deq-member(eq;x;L),  atom_eq: atomeqn def
Definitions :  eqof: eqof(d),  lambda: x.A[x],  member: t  T,  sqequal: s ~ t,  equal: s = t,  function: x:A  B[x],  all: x:A. B[x],  top: Top,  uall: [x:A]. B[x],  Auto: Error :Auto,  CollapseTHEN: Error :CollapseTHEN,  tactic: Error :tactic
Lemmas :  top_wf

---

\mforall{}[x,L:Top].    (rec-case(L)  of  []  =>  ff  |  a::$_{}$  =>  r.if  a=2  x  then  tt  else  r  \msim{}  \000Cdeq-member(IdDeq;x;L))


Date html generated: 2011_08_10-AM-07_52_49
Last ObjectModification: 2011_06_18-AM-08_14_46

Home Index