---

Step * 1 of Lemma union-continuous-type-monotone

.....wf..... 
1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. union-continuous{i:l}(T.F[T])
4. A : Type
5. B : Type
6. A ⊆r B
7. x : F A@i
⊢ x ∈ F B
BY
{ ((With ⌜𝔹⌝ (D 3)⋅ THENA Auto)
   THEN ((InstHyp [⌜λb.if b then A else B fi ⌝] (-1)⋅ THENM Reduce (-1)) THENA Auto)
   THEN SubsumeC ⌜⋃n:𝔹.F[if n then A else B fi ]⌝⋅
   THEN Try ((MemTypeCDUnion ⌜tt⌝⋅ THEN Auto)⋅)) }

1
1. F : Type ⟶ Type
2. ∀A,B:Type.  (A ≡ B ⇒ F[A] ≡ F[B])
3. A : Type
4. B : Type
5. A ⊆r B
6. x : F A@i
7. ∀[X:𝔹 ⟶ Type]. (⋃n:𝔹.F[X n] ⊆r F[⋃n:𝔹.(X n)])
8. ⋃n:𝔹.F[if n then A else B fi ] ⊆r F[⋃n:𝔹.if n then A else B fi ]
9. x = x ∈ ⋃n:𝔹.F[if n then A else B fi ]
⊢ ⋃n:𝔹.F[if n then A else B fi ] ⊆r (F B)

---

Latex:

---

Latex:
.....wf..... 
1.  F  :  Type  {}\mrightarrow{}  Type
2.  \mforall{}A,B:Type.    (A  \mequiv{}  B  {}\mRightarrow{}  F[A]  \mequiv{}  F[B])
3.  union-continuous\{i:l\}(T.F[T])
4.  A  :  Type
5.  B  :  Type
6.  A  \msubseteq{}r  B
7.  x  :  F  A@i
\mvdash{}  x  \mmember{}  F  B


By

---

Latex:
((With  \mkleeneopen{}\mBbbB{}\mkleeneclose{}  (D  3)\mcdot{}  THENA  Auto)
  THEN  ((InstHyp  [\mkleeneopen{}\mlambda{}b.if  b  then  A  else  B  fi  \mkleeneclose{}]  (-1)\mcdot{}  THENM  Reduce  (-1))  THENA  Auto)
  THEN  SubsumeC  \mkleeneopen{}\mcup{}n:\mBbbB{}.F[if  n  then  A  else  B  fi  ]\mkleeneclose{}\mcdot{}
  THEN  Try  ((MemTypeCDUnion  \mkleeneopen{}tt\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}))

---

Home Index