---

Step * of Lemma face-lattice1-is-inc

∀T:Type. ∀eq:EqDecider(T). ∀x:T.  ((x=1) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr x ))
BY
{ (Auto
   THEN RepUR ``face-lattice1 free-dlwc-inc face-lattice-constraints`` 0
   THEN (RepUR ``fset-filter fset-singleton fset-null`` 0 THEN Fold `fset-singleton` 0)
   THEN Subst' deq-f-subset(union-deq(T;T;eq;eq)) {inl x,inr x } {inr x } ~ ff 0
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x:T.
    ((x=1)  \msim{}  free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inr  x  ))


By

---

Latex:
(Auto
  THEN  RepUR  ``face-lattice1  free-dlwc-inc  face-lattice-constraints``  0
  THEN  (RepUR  ``fset-filter  fset-singleton  fset-null``  0  THEN  Fold  `fset-singleton`  0)
  THEN  Subst'  deq-f-subset(union-deq(T;T;eq;eq))  \{inl  x,inr  x  \}  \{inr  x  \}  \msim{}  ff  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index