Step
*
of Lemma
aa_capply_wf
[a1,a:Type]. [p:a 
]. [l:a 
a1]. (aa_capply(p;l) 
a1 )
BY
{ ProveWfLemma }
\mforall{}[a1,a:Type]. \mforall{}[p:a \mtimes{} \mBbbZ{}]. \mforall{}[l:a {}\mrightarrow{} a1]. (aa\_capply(p;l) \mmember{} a1 \mtimes{} \mBbbZ{})
By
ProveWfLemma
Home
Index