Step
*
of Lemma
face-lattice0-is-inc
No Annotations
∀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:
No Annotations
\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