---

Step * 1 1 of Lemma face-lattice0-is-inc


1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : T@i
4. inl x ∈ T + T
5. inr x  ∈ T + T
6. {inl x,inr x } ⊆ {inl x}@i
⊢ False
BY
{ ((With ⌜inr x ⌝ (D (-1))⋅ THEN Auto)
   THEN (D -1 THENA (RWO  "member-fset-pair" 0 THEN Auto))
   THEN RWO  "member-fset-singleton" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type@i'
2.  eq  :  EqDecider(T)@i
3.  x  :  T@i
4.  inl  x  \mmember{}  T  +  T
5.  inr  x    \mmember{}  T  +  T
6.  \{inl  x,inr  x  \}  \msubseteq{}  \{inl  x\}@i
\mvdash{}  False


By

---

Latex:
((With  \mkleeneopen{}inr  x  \mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)
  THEN  (D  -1  THENA  (RWO    "member-fset-pair"  0  THEN  Auto))
  THEN  RWO    "member-fset-singleton"  (-1)
  THEN  Auto)

---

Home Index