{ pDVcontinue()  PiDataVal() }

{ Proof }



Definitions occuring in Statement :  pDVcontinue: pDVcontinue() PiDataVal: PiDataVal() member: t  T
Definitions :  equal: s = t member: t  T function: x:A  B[x] all: x:A. B[x] name: Name product: x:A  B[x] pi_prefix: pi_prefix() list: type List universe: Type nat: unit: Unit Id: Id union: left + right it: inl: inl x  inr: inr x  pDVcontinue: pDVcontinue() PiDataVal: PiDataVal()
Lemmas :  it_wf Id_wf unit_wf nat_wf pi_prefix_wf name_wf

pDVcontinue()  \mmember{}  PiDataVal()


Date html generated: 2010_08_27-PM-08_42_47
Last ObjectModification: 2010_04_23-AM-11_30_55

Home Index