Step
*
of Lemma
no_repeats_witness
∀[T:Type]. ∀[l:T List]. (no_repeats(T;l)
⇒ (λx.Ax ∈ no_repeats(T;l)))
BY
{ (Auto THEN ProveTrivialWitness THEN Auto THEN Fold `uall` 3 THEN InstHyp [⌜i⌝;⌜j⌝] 3⋅ THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[l:T List]. (no\_repeats(T;l) {}\mRightarrow{} (\mlambda{}x.Ax \mmember{} no\_repeats(T;l)))
By
Latex:
(Auto THEN ProveTrivialWitness THEN Auto THEN Fold `uall` 3 THEN InstHyp [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}] 3\mcdot{} THEN Auto)
Home
Index