Step
*
of Lemma
face-lattice1_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ((x=1) ∈ Point(face-lattice(T;eq)))
BY
{ (Auto
THEN (InstLemma `free-dlwc-inc_wf` [⌜T + T⌝;⌜union-deq(T;T;eq;eq)⌝;⌜λ2x.face-lattice-constraints(x)⌝;⌜inr x ⌝]⋅
THENA Auto
)
THEN Fold `face-lattice` (-1)
THEN (NthHypSq (-1) THEN EqCD)
THEN Auto) }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[eq:EqDecider(T)]. \mforall{}[x:T]. ((x=1) \mmember{} Point(face-lattice(T;eq)))
By
Latex:
(Auto
THEN (InstLemma `free-dlwc-inc\_wf` [\mkleeneopen{}T + T\mkleeneclose{};\mkleeneopen{}union-deq(T;T;eq;eq)\mkleeneclose{};
\mkleeneopen{}\mlambda{}\msubtwo{}x.face-lattice-constraints(x)\mkleeneclose{};\mkleeneopen{}inr x \mkleeneclose{}]\mcdot{}
THENA Auto
)
THEN Fold `face-lattice` (-1)
THEN (NthHypSq (-1) THEN EqCD)
THEN Auto)
Home
Index