Step
*
of Lemma
dM-meet-inc-opp
∀[i:ℕ]. (<i> ∧ <1-i> ~ {{inr i ,inl i}})
BY
{ (Auto THEN Repeat ((Computation THEN (Reduce 0 THENA Auto)))) }
Latex:
Latex:
\mforall{}[i:\mBbbN{}].  (<i>  \mwedge{}  ə-i>  \msim{}  \{\{inr  i  ,inl  i\}\})
By
Latex:
(Auto  THEN  Repeat  ((Computation  THEN  (Reduce  0  THENA  Auto))))
Home
Index