---

Step * 1 of Lemma fl-meet-0-1

.....assertion..... 
1. T : Type
2. eq : EqDecider(T)
3. x : T
⊢ ∀x:T + T. ∀c:fset(T + T).  (c ∈ face-lattice-constraints(x) ⇒ x ∈ c)
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN RepUR ``face-lattice-constraints`` 0
   THEN RenameVar `z' (-1)
   THEN (Assert inl z ∈ T + T BY
               Auto)
   THEN (Assert inr z  ∈ T + T BY
               Auto)
   THEN Auto
   THEN (RWO "member-fset-singleton" (-1)⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN EAuto 1) }

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  T
\mvdash{}  \mforall{}x:T  +  T.  \mforall{}c:fset(T  +  T).    (c  \mmember{}  face-lattice-constraints(x)  {}\mRightarrow{}  x  \mmember{}  c)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``face-lattice-constraints``  0
  THEN  RenameVar  `z'  (-1)
  THEN  (Assert  inl  z  \mmember{}  T  +  T  BY
                          Auto)
  THEN  (Assert  inr  z    \mmember{}  T  +  T  BY
                          Auto)
  THEN  Auto
  THEN  (RWO  "member-fset-singleton"  (-1)\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  EAuto  1)

---

Home Index