---

Step * 2 of Lemma WfdSpread-ext

.....subterm..... T:t
1:n
1. Pos : Type
2. ∀a,b:Pos.  Dec(a = b ∈ Pos)
3. Mv : Pos ⟶ Type
4. Spread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))
5. x : a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
⊢ x ∈ WfdSpread(Pos;a.Mv[a])
BY
{ TACTIC:(Assert x ∈ Spread(Pos;a.Mv[a]) BY
                (D 4 THEN SubsumeC a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))⋅ THEN Auto)) }

1
1. Pos : Type
2. ∀a,b:Pos.  Dec(a = b ∈ Pos)
3. Mv : Pos ⟶ Type
4. Spread(Pos;a.Mv[a]) ≡ a:Pos × (Mv[a] ⟶ Spread(Pos;a.Mv[a]))
5. x : a:Pos × (Mv[a] ⟶ WfdSpread(Pos;a.Mv[a]))
6. x ∈ Spread(Pos;a.Mv[a])
⊢ x ∈ WfdSpread(Pos;a.Mv[a])

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  Pos  :  Type
2.  \mforall{}a,b:Pos.    Dec(a  =  b)
3.  Mv  :  Pos  {}\mrightarrow{}  Type
4.  Spread(Pos;a.Mv[a])  \mequiv{}  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a]))
5.  x  :  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  WfdSpread(Pos;a.Mv[a]))
\mvdash{}  x  \mmember{}  WfdSpread(Pos;a.Mv[a])


By

---

Latex:
TACTIC:(Assert  x  \mmember{}  Spread(Pos;a.Mv[a])  BY
                            (D  4  THEN  SubsumeC  a:Pos  \mtimes{}  (Mv[a]  {}\mrightarrow{}  Spread(Pos;a.Mv[a]))\mcdot{}  THEN  Auto))

---

Home Index