---

Step * 2 of Lemma dm-neg-is-hom-opposite

.....set predicate..... 
1. T : Type
2. eq : EqDecider(T)
⊢ (((λx.¬(x)) 0) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ (((λx.¬(x)) 1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))
BY
{ (Reduce 0 THEN Subst' 0 ~ 1 0) }

1
.....equality..... 
1. T : Type
2. eq : EqDecider(T)
⊢ 0 ~ 1

2
1. T : Type
2. eq : EqDecider(T)
⊢ (¬(1) = 0 ∈ Point(free-DeMorgan-lattice(T;eq))) ∧ (¬(1) = 1 ∈ Point(free-DeMorgan-lattice(T;eq)))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  (((\mlambda{}x.\mneg{}(x))  0)  =  0)  \mwedge{}  (((\mlambda{}x.\mneg{}(x))  1)  =  1)


By

---

Latex:
(Reduce  0  THEN  Subst'  0  \msim{}  1  0)

---

Home Index