{ [x:pi_prefix()]. (pircv?(x)  ) }

{ Proof }



Definitions occuring in Statement :  pircv?: pircv?(x) pi_prefix: pi_prefix() bool: uall: [x:A]. B[x] member: t  T
Definitions :  uall: [x:A]. B[x] member: t  T pircv?: pircv?(x) so_lambda: x y.t[x; y] so_apply: x[s1;s2]
Lemmas :  pi_prefix_ind_wf bool_wf bfalse_wf name_wf btrue_wf pi_prefix_wf

\mforall{}[x:pi\_prefix()].  (pircv?(x)  \mmember{}  \mBbbB{})


Date html generated: 2011_08_17-PM-06_41_02
Last ObjectModification: 2011_06_18-PM-12_08_06

Home Index