Step
*
1
1
1
1
1
1
1
1
1
of Lemma
groupoid-edges-commute1
1. i : ℕ2
⊢ i = i ∈ ℕ2
BY
{ TACTIC:Auto }
Latex:
Latex:
1.  i  :  \mBbbN{}2
\mvdash{}  i  =  i
By
Latex:
TACTIC:Auto
Home
Index