---

{ [x:ClassDerivation]
    cdvcomb-arg(x)  ClassDerivation supposing cdvcomb?(x) }

{ Proof }

---

Definitions occuring in Statement :  cdvcomb-arg: cdvcomb-arg(x),  cdvcomb?: cdvcomb?(x),  classderiv: ClassDerivation,  assert: b,  uimplies: b supposing a,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  classderiv: ClassDerivation,  uimplies: b supposing a,  assert: b,  cdvcomb?: cdvcomb?(x),  member: t  T,  cdvcomb-arg: cdvcomb-arg(x),  implies: P  Q,  bfalse: ff,  btrue: tt,  ifthenelse: if b then t else f fi ,  unit: Unit,  false: False,  it: ,  cdvbase: cdvbase(args),  prop: ,  cdvpair: cdvpair(fst;snd),  cdvdelay: cdvdelay(X;dummy),  cdvcomb: cdvcomb(typ;argtype;arg;fun),  cdvreccomb: cdvreccomb(typ;argtype;arg;fun)
Lemmas :  classderiv_wf,  false_wf,  true_wf,  assert_wf,  cdvcomb?_wf

---

\mforall{}[x:ClassDerivation].  cdvcomb-arg(x)  \mmember{}  ClassDerivation  supposing  \muparrow{}cdvcomb?(x)


Date html generated: 2011_08_17-PM-04_25_18
Last ObjectModification: 2011_06_18-AM-11_37_38

Home Index