Step
*
of Lemma
RankEx2_Prod_wf
∀[S,T:Type]. ∀[prod:RankEx2(S;T) × S × T]. (RankEx2_Prod(prod) ∈ RankEx2(S;T))
BY
{ DepprodCoDatatypeConstructorWf `RankEx2_size` }
Latex:
\mforall{}[S,T:Type]. \mforall{}[prod:RankEx2(S;T) \mtimes{} S \mtimes{} T]. (RankEx2\_Prod(prod) \mmember{} RankEx2(S;T))
By
DepprodCoDatatypeConstructorWf `RankEx2\_size`
Home
Index