Step
*
of Lemma
l-all-iff
∀[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)} ⟶ ℙ]. (∀x∈L.P[x]
⇐⇒ (∀x∈L.P[x]))
BY
{ (Assert ⌜∀[T:Type]. ∀L:T List. ∀[P:T ⟶ ℙ]. (∀x∈L.P[x]
⇐⇒ (∀x∈L.P[x]))⌝⋅
THEN Try (((UnivCD THENM (InstHyp [⌜{a:T| (a ∈ L)} ⌝; ⌜L⌝; ⌜P⌝] 1)⋅) THEN Auto))
THEN (InductionOnList THENA Auto)
THEN Unfold `l-all` 0
THEN Reduce 0
THEN Try (Fold `l-all` 0)
THEN Intro
THEN RWW "l_all_cons" 0
THEN Auto
THEN Try ((BackThruSomeHyp THEN Auto))
THEN (D (-1) THEN Auto THEN BLemma `l_all_nil` THEN Auto)⋅) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}L:T List. \mforall{}[P:\{x:T| (x \mmember{} L)\} {}\mrightarrow{} \mBbbP{}]. (\mforall{}x\mmember{}L.P[x] \mLeftarrow{}{}\mRightarrow{} (\mforall{}x\mmember{}L.P[x]))
By
Latex:
(Assert \mkleeneopen{}\mforall{}[T:Type]. \mforall{}L:T List. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. (\mforall{}x\mmember{}L.P[x] \mLeftarrow{}{}\mRightarrow{} (\mforall{}x\mmember{}L.P[x]))\mkleeneclose{}\mcdot{}
THEN Try (((UnivCD THENM (InstHyp [\mkleeneopen{}\{a:T| (a \mmember{} L)\} \mkleeneclose{}; \mkleeneopen{}L\mkleeneclose{}; \mkleeneopen{}P\mkleeneclose{}] 1)\mcdot{}) THEN Auto))
THEN (InductionOnList THENA Auto)
THEN Unfold `l-all` 0
THEN Reduce 0
THEN Try (Fold `l-all` 0)
THEN Intro
THEN RWW "l\_all\_cons" 0
THEN Auto
THEN Try ((BackThruSomeHyp THEN Auto))
THEN (D (-1) THEN Auto THEN BLemma `l\_all\_nil` THEN Auto)\mcdot{})
Home
Index