---

Step * 1 of Lemma free-dma-lift_wf


1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
⊢ TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} T eq dm eq2 f ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| 
                                                                      ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} 
BY
{ Subst' TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} ~ TERMOF{free-DeMorgan-algebra-property:o, 1:l, i:l} 0 }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
⊢ TERMOF{free-DeMorgan-algebra-property:o, 1:l, 1:l} ~ TERMOF{free-DeMorgan-algebra-property:o, 1:l, i:l}

2
1. T : Type
2. eq : EqDecider(T)
3. dm : DeMorganAlgebra
4. eq2 : EqDecider(Point(dm))
5. f : T ⟶ Point(dm)
⊢ TERMOF{free-DeMorgan-algebra-property:o, 1:l, i:l} T eq dm eq2 f ∈ {g:dma-hom(free-DeMorgan-algebra(T;eq);dm)| 
                                                                      ∀i:T. ((g <i>) = (f i) ∈ Point(dm))} 

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  dm  :  DeMorganAlgebra
4.  eq2  :  EqDecider(Point(dm))
5.  f  :  T  {}\mrightarrow{}  Point(dm)
\mvdash{}  TERMOF\{free-DeMorgan-algebra-property:o,  1:l,  1:l\}  T  eq  dm  eq2  f
    \mmember{}  \{g:dma-hom(free-DeMorgan-algebra(T;eq);dm)|  \mforall{}i:T.  ((g  <i>)  =  (f  i))\} 


By

---

Latex:
Subst'  TERMOF\{free-DeMorgan-algebra-property:o,  1:l,  1:l\}  \msim{}  TERMOF\{free-DeMorgan-algebra-property:o,
                                                                                                                                      1:l,
                                                                                                                                      i:l\}  0

---

Home Index