---

Step * 1 1 1 1 of Lemma trivial_sym_grp


1. f : ℕ1 ⟶ ℕ1
2. p1 : ℕ1 ⟶ ℕ1
3. InvFuns(ℕ1;ℕ1;<f, p1>.f;<f, p1>.b)
⊢ <f, p1> = <Id, Id> ∈ (f:ℕ1 ⟶ ℕ1 × (ℕ1 ⟶ ℕ1))
BY
{ ((EqCD THEN Try (BackThruLemma `trivial_nat1_fun`)) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}1  {}\mrightarrow{}  \mBbbN{}1
2.  p1  :  \mBbbN{}1  {}\mrightarrow{}  \mBbbN{}1
3.  InvFuns(\mBbbN{}1;\mBbbN{}1;<f,  p1>.f;<f,  p1>.b)
\mvdash{}  <f,  p1>  =  <Id,  Id>


By

---

Latex:
((EqCD  THEN  Try  (BackThruLemma  `trivial\_nat1\_fun`))  THEN  Auto)

---

Home Index