Step
*
1
1
1
of Lemma
dm-neg-opp
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. i : T
⊢ λz.case z of inl(a) => {{inr a }} | inr(a) => {{inl a}} ∈ (T + T) ⟶ Point(free-DeMorgan-lattice(T;eq))
BY
{ ((MemCD THENA Auto)
THEN D -1
THEN Reduce 0
THEN Fold `free-dl-inc` 0
THEN Unfold `free-DeMorgan-lattice` 0
THEN Auto) }
Latex:
Latex:
.....assertion.....
1. T : Type
2. eq : EqDecider(T)
3. i : T
\mvdash{} \mlambda{}z.case z of inl(a) => \{\{inr a \}\} | inr(a) => \{\{inl a\}\} \mmember{} (T + T)
{}\mrightarrow{} Point(free-DeMorgan-lattice(T;eq))
By
Latex:
((MemCD THENA Auto)
THEN D -1
THEN Reduce 0
THEN Fold `free-dl-inc` 0
THEN Unfold `free-DeMorgan-lattice` 0
THEN Auto)
Home
Index