Step
*
of Lemma
ispair_wf_list
∀[T:Type]. ∀[L:T List]. (ispair(L) ∈ 𝔹)
BY
{ (InductionOnList THEN Reduce 0 THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[L:T List]. (ispair(L) \mmember{} \mBbbB{})
By
Latex:
(InductionOnList THEN Reduce 0 THEN Auto)
Home
Index