---

Step * 1 1 1 1 of Lemma txpose_perm_order_2


1. n : ℕ
2. i : ℕn
3. j : ℕn
⊢ id_perm() ∈ perm_sig(ℕn)
BY
{ % silly subgoal left over since we are not doing 
  haven't bothered yet to do type inclusion  
   matching on equality type % 
 
Unfold `id_perm` 0 THEN Auto 
⋅ }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n
3.  j  :  \mBbbN{}n
\mvdash{}  id\_perm()  \mmember{}  perm\_sig(\mBbbN{}n)


By

---

Latex:
\%  silly  subgoal  left  over  since  we  are  not  doing 
    haven't  bothered  yet  to  do  type  inclusion   
      matching  on  equality  type  \% 
 
Unfold  `id\_perm`  0  THEN  Auto 
\mcdot{}

---

Home Index