Step
*
1
2
1
of Lemma
fpf-sub-val2
1. A : Type
2. A' : Type
3. strong-subtype(A;A')
4. B : A ─→ Type
5. eq : EqDecider(A')@i
6. d1 : A List@i
7. f1 : a:{a:A| (a ∈ d1)} ─→ B[a]@i
8. d : A List@i
9. g1 : a:{a:A| (a ∈ d)} ─→ B[a]@i
10. x : A'@i
11. P : a:A ─→ B[a] ─→ ℙ
12. Q : a:A ─→ B[a] ─→ ℙ
13. ∀x:A. ∀z:B[x]. (P[x;z]
⇒ Q[x;z])@i
14. eq ∈ EqDecider(A)
15. <d, g1> ⊆ <d1, f1>
16. ↑x ∈b d1)
⊢ x ∈ A
BY
{ ((RWO "assert-deq-member" (-1))
THEN Auto
THEN (Using [`L',⌈d1⌉] (BLemma `strong-subtype-l_member-type`))⋅
THEN Auto) }
Latex:
1. A : Type
2. A' : Type
3. strong-subtype(A;A')
4. B : A {}\mrightarrow{} Type
5. eq : EqDecider(A')@i
6. d1 : A List@i
7. f1 : a:\{a:A| (a \mmember{} d1)\} {}\mrightarrow{} B[a]@i
8. d : A List@i
9. g1 : a:\{a:A| (a \mmember{} d)\} {}\mrightarrow{} B[a]@i
10. x : A'@i
11. P : a:A {}\mrightarrow{} B[a] {}\mrightarrow{} \mBbbP{}
12. Q : a:A {}\mrightarrow{} B[a] {}\mrightarrow{} \mBbbP{}
13. \mforall{}x:A. \mforall{}z:B[x]. (P[x;z] {}\mRightarrow{} Q[x;z])@i
14. eq \mmember{} EqDecider(A)
15. <d, g1> \msubseteq{} <d1, f1>
16. \muparrow{}x \mmember{}\msubb{} d1)
\mvdash{} x \mmember{} A
By
((RWO "assert-deq-member" (-1))
THEN Auto
THEN (Using [`L',\mkleeneopen{}d1\mkleeneclose{}] (BLemma `strong-subtype-l\_member-type`))\mcdot{}
THEN Auto)
Home
Index