---

Step * of Lemma aa_capply_wf2

p:Base  . l:Base  Base.  (aa_capply(p;l)  Base  )
BY
{ ProveWfLemma }

1
.....set predicate..... 
1. p : Base  @i
2. l : Base  Base@i
 0  (1 + (snd(p)))


\mforall{}p:Base  \mtimes{}  \mBbbN{}.  \mforall{}l:Base  {}\mrightarrow{}  Base.    (aa\_capply(p;l)  \mmember{}  Base  \mtimes{}  \mBbbN{})


By

ProveWfLemma



Home Index