Step
*
of Lemma
l_all-squash-exists-list
∀[A,B:Type]. ∀[as:A List]. ∀[P:A ⟶ B ⟶ ℙ].
↓∃bs:(A × B) List. ((map(λx.(fst(x));bs) = as ∈ (A List)) ∧ (∀x∈bs.↓P[fst(x);snd(x)])) supposing (∀x∈as.↓∃y:B. P[x;y])
BY
{ (Auto
THEN ListInd (-3)
THEN Auto
THEN Try (Complete ((D 0 THEN InstConcl [⌜[]⌝]⋅ THEN Reduce 0 THEN Auto)))
THEN (RW ListC (-1) THENA Auto)
THEN D (-2)
THEN Auto
THEN ExRepD
THEN D 0
THEN InstConcl [⌜[<u, y> / bs]⌝]⋅
THEN Reduce 0
THEN Auto
THEN RW ListC 0
THEN Reduce 0
THEN Auto) }
Latex:
Latex:
\mforall{}[A,B:Type]. \mforall{}[as:A List]. \mforall{}[P:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}].
\mdownarrow{}\mexists{}bs:(A \mtimes{} B) List. ((map(\mlambda{}x.(fst(x));bs) = as) \mwedge{} (\mforall{}x\mmember{}bs.\mdownarrow{}P[fst(x);snd(x)]))
supposing (\mforall{}x\mmember{}as.\mdownarrow{}\mexists{}y:B. P[x;y])
By
Latex:
(Auto
THEN ListInd (-3)
THEN Auto
THEN Try (Complete ((D 0 THEN InstConcl [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{} THEN Reduce 0 THEN Auto)))
THEN (RW ListC (-1) THENA Auto)
THEN D (-2)
THEN Auto
THEN ExRepD
THEN D 0
THEN InstConcl [\mkleeneopen{}[<u, y> / bs]\mkleeneclose{}]\mcdot{}
THEN Reduce 0
THEN Auto
THEN RW ListC 0
THEN Reduce 0
THEN Auto)
Home
Index