---

Step * 1 of Lemma aa_capply_wf2

.....set predicate..... 
1. p : Base  @i
2. l : Base  Base@i
 0  (1 + (snd(p)))
BY
{ (Assert snd(p)   THEN Auto') }


.....set  predicate..... 
1.  p  :  Base  \mtimes{}  \mBbbN{}@i
2.  l  :  Base  {}\mrightarrow{}  Base@i
\mvdash{}  0  \mleq{}  (1  +  (snd(p)))


By

(Assert  \mkleeneopen{}snd(p)  \mmember{}  \mBbbN{}\mkleeneclose{}\mcdot{}  THEN  Auto')



Home Index