Step
*
of Lemma
in-first-eclass
∀[Info,A:Type]. ∀Xs:EClass(A) List. ∀es:EO+(Info). ∀e:E. (↑e ∈b first-eclass(Xs)
⇐⇒ (∃X∈Xs. ↑e ∈b X))
BY
{ (At ⌈𝕌'⌉InductionOnLast⋅ THEN (RWW "l_exists_cons l_exists_nil" 0 THENA Auto)) }
1
1. [Info] : Type
2. [A] : Type
⊢ ∀es:EO+(Info). ∀e:E. (↑e ∈b first-eclass([])
⇐⇒ False)
2
1. [Info] : Type
2. [A] : Type
3. Xs : EClass(A) List@i'
4. ¬↑null(Xs)
5. ||Xs|| ≥ 1
6. ∀es:EO+(Info). ∀e:E. (↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs))
⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs). ↑e ∈b X))
⊢ ∀es:EO+(Info). ∀e:E.
(↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs) @ [last(Xs)])
⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs) @ [last(Xs)]. ↑e ∈b X))
Latex:
Latex:
\mforall{}[Info,A:Type].
\mforall{}Xs:EClass(A) List. \mforall{}es:EO+(Info). \mforall{}e:E. (\muparrow{}e \mmember{}\msubb{} first-eclass(Xs) \mLeftarrow{}{}\mRightarrow{} (\mexists{}X\mmember{}Xs. \muparrow{}e \mmember{}\msubb{} X))
By
Latex:
(At \mkleeneopen{}\mBbbU{}'\mkleeneclose{}InductionOnLast\mcdot{} THEN (RWW "l\_exists\_cons l\_exists\_nil" 0 THENA Auto))
Home
Index