Step
*
of Lemma
RankEx2_LeafS-leafs_wf
∀[S,T:Type]. ∀[v:RankEx2(S;T)]. RankEx2_LeafS-leafs(v) ∈ S supposing ↑RankEx2_LeafS?(v)
BY
{ DepprodCoDatatypeSelectorWf }
Latex:
\mforall{}[S,T:Type]. \mforall{}[v:RankEx2(S;T)]. RankEx2\_LeafS-leafs(v) \mmember{} S supposing \muparrow{}RankEx2\_LeafS?(v)
By
DepprodCoDatatypeSelectorWf
Home
Index