---

Step * of Lemma face-lattice0-is-inc

∀T:Type. ∀eq:EqDecider(T). ∀x:T.  ((x=0) ~ free-dlwc-inc(union-deq(T;T;eq;eq);a.face-lattice-constraints(a);inl x))
BY
{ (Auto
   THEN RepUR ``face-lattice0 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 } {inl x} ~ ff 0
   THEN Reduce 0
   THEN Auto) }

1
1. T : Type@i'
2. eq : EqDecider(T)@i
3. x : T@i
⊢ deq-f-subset(union-deq(T;T;eq;eq)) {inl x,inr x } {inl x} = ff

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  RepUR  ``face-lattice0  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  \}  \{inl  x\}  \msim{}  ff  0
  THEN  Reduce  0
  THEN  Auto)

---

Home Index