Step
*
2
1
1
1
of Lemma
co-regext-loopset
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. t : coW(Unit;x.Unit)
3. T : 𝕌'
4. ((a:Type × (a ⟶ T)) ⊆r T) ∧ (coSet{i:l} ⊆r T)
⊢ (regextfun(λp.loopset();t) = loopset() ∈ T) 
⇒ (regextfun(λp.loopset();t) = loopset() ∈ (a:Type × (a ⟶ T)))
BY
{ (D -1 THEN (D 0 THENA Auto)) }
1
1. ∀t:coW(Unit;x.Unit). (regextfun(λp.loopset();t) ∈ coSet{i:l})
2. t : coW(Unit;x.Unit)
3. T : 𝕌'
4. (a:Type × (a ⟶ T)) ⊆r T
5. coSet{i:l} ⊆r T
6. regextfun(λp.loopset();t) = loopset() ∈ T
⊢ regextfun(λp.loopset();t) = loopset() ∈ (a:Type × (a ⟶ T))
Latex:
Latex:
1.  \mforall{}t:coW(Unit;x.Unit).  (regextfun(\mlambda{}p.loopset();t)  \mmember{}  coSet\{i:l\})
2.  t  :  coW(Unit;x.Unit)
3.  T  :  \mBbbU{}'
4.  ((a:Type  \mtimes{}  (a  {}\mrightarrow{}  T))  \msubseteq{}r  T)  \mwedge{}  (coSet\{i:l\}  \msubseteq{}r  T)
\mvdash{}  (regextfun(\mlambda{}p.loopset();t)  =  loopset())  {}\mRightarrow{}  (regextfun(\mlambda{}p.loopset();t)  =  loopset())
By
Latex:
(D  -1  THEN  (D  0  THENA  Auto))
Home
Index