---

Step * 1 of Lemma fl-point


1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6. ↑fset-antichain(union-deq(T;T;eq;eq);x)
7. a : fset(T + T)
8. a ∈ x
9. z : T
⊢ ¬(inl z ∈ a ∧ inr z  ∈ a)
BY
{ ((InstLemma `fset-all-iff` [⌜fset(T + T)⌝;⌜deq-fset(union-deq(T;T;eq;eq))⌝]⋅ THENA Auto)
   THEN (RWO "-1" 5 THENA Auto)
   THEN Thin (-1)
   THEN (InstHyp [⌜a⌝] 5⋅ THENA Auto)
   THEN Thin 5
   THEN RWO "assert-fset-contains-none" (-1)
   THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)
3. x : fset(fset(T + T))
4. ↑fset-antichain(union-deq(T;T;eq;eq);x)
5. ↑fset-antichain(union-deq(T;T;eq;eq);x)
6. a : fset(T + T)
7. a ∈ x
8. z : T
9. ∀x:T + T. (x ∈ a ⇒ (∀c:fset(T + T). (c ∈ face-lattice-constraints(x) ⇒ (¬c ⊆ a))))
⊢ ¬(inl z ∈ a ∧ inr z  ∈ a)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  fset(fset(T  +  T))
4.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
5.  fset-all(x;a.fset-contains-none(union-deq(T;T;eq;eq);a;x.face-lattice-constraints(x)))
6.  \muparrow{}fset-antichain(union-deq(T;T;eq;eq);x)
7.  a  :  fset(T  +  T)
8.  a  \mmember{}  x
9.  z  :  T
\mvdash{}  \mneg{}(inl  z  \mmember{}  a  \mwedge{}  inr  z    \mmember{}  a)


By

---

Latex:
((InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T  +  T)\mkleeneclose{};\mkleeneopen{}deq-fset(union-deq(T;T;eq;eq))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  5  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  Thin  5
  THEN  RWO  "assert-fset-contains-none"  (-1)
  THEN  Auto)

---

Home Index