Step
*
of Lemma
sqlen_sqequaln
∀[a,b:Base]. ∀[n:ℕ]. a ≤n b supposing a ~n b
BY
{ Intros }
1
1. [a] : Base
2. [b] : Base
3. [n] : ℕ
4. [%] : a ~n b
⊢ a ≤n b
Latex:
Latex:
\mforall{}[a,b:Base]. \mforall{}[n:\mBbbN{}]. a \mleq{}n b supposing a \msim{}n b
By
Latex:
Intros
Home
Index