Step
*
of Lemma
band-simple-decide
∀[a,b:Top]. (case a of inl(y) => inl ⋅ | inr(z) => inr ⋅ ∧b b ~ case a of inl(y) => b | inr(z) => inr ⋅ )
BY
{ (RW (BasicSymbolicComputeC []) 0 THEN Auto) }
Latex:
Latex:
\mforall{}[a,b:Top].
(case a of inl(y) => inl \mcdot{} | inr(z) => inr \mcdot{} \mwedge{}\msubb{} b \msim{} case a of inl(y) => b | inr(z) => inr \mcdot{} )
By
Latex:
(RW (BasicSymbolicComputeC []) 0 THEN Auto)
Home
Index