Step
*
1
1
1
1
of Lemma
all-quotient-dependent
.....assertion.....
1. T : Type
2. c : T ⟶ Base
3. ∀x:T. (c x ∈ T ⋂ Base)
4. ∀x:T. ((c x) = x ∈ T)
5. S : T ⟶ ℙ
6. E : t:T ⟶ (S t) ⟶ (S t) ⟶ ℙ
7. ∀t:T. EquivRel(S t;a,b.E t a b)
8. f : t:T ⟶ (x,y:S t//(E t x y))
⊢ f,g:∀x:T ⋂ Base. (S x)//(∀x:T ⋂ Base. (↓E x (f x) (g x)))
BY
{ ((UseWitness ⌜f⌝⋅ THEN Auto) THEN SubsumeC ⌜t:T ⋂ Base ⟶ (x,y:S t//(E t x y))⌝⋅ THEN Auto) }
Latex:
Latex:
.....assertion.....
1. T : Type
2. c : T {}\mrightarrow{} Base
3. \mforall{}x:T. (c x \mmember{} T \mcap{} Base)
4. \mforall{}x:T. ((c x) = x)
5. S : T {}\mrightarrow{} \mBbbP{}
6. E : t:T {}\mrightarrow{} (S t) {}\mrightarrow{} (S t) {}\mrightarrow{} \mBbbP{}
7. \mforall{}t:T. EquivRel(S t;a,b.E t a b)
8. f : t:T {}\mrightarrow{} (x,y:S t//(E t x y))
\mvdash{} f,g:\mforall{}x:T \mcap{} Base. (S x)//(\mforall{}x:T \mcap{} Base. (\mdownarrow{}E x (f x) (g x)))
By
Latex:
((UseWitness \mkleeneopen{}f\mkleeneclose{}\mcdot{} THEN Auto) THEN SubsumeC \mkleeneopen{}t:T \mcap{} Base {}\mrightarrow{} (x,y:S t//(E t x y))\mkleeneclose{}\mcdot{} THEN Auto)
Home
Index