Step
*
of Lemma
decidable__equal-fl-point
No Annotations
∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(face-lattice(T;eq)). Dec(x = y ∈ Point(face-lattice(T;eq)))
BY
{ TACTIC:(Auto THEN All (RWO "fl-point-sq") THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[T:Type]. \mforall{}eq:EqDecider(T). \mforall{}x,y:Point(face-lattice(T;eq)). Dec(x = y)
By
Latex:
TACTIC:(Auto THEN All (RWO "fl-point-sq") THEN Auto)
Home
Index