---

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


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

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

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
\mvdash{}  (\mneg{}(1)  =  0)  \mwedge{}  (\mneg{}(1)  =  1)


By

---

Latex:
Subst'  1  \msim{}  0  0

---

Home Index