---

Step * of Lemma rel_exp-one-one

∀[B:Type]. ∀[R:B ⟶ B ⟶ ℙ].  ∀[n:ℕ]. one-one(B;B;R^n) supposing one-one(B;B;R)
BY
{ (InductionOnNat
   THEN (D 0 THENA Auto)
   THEN RecUnfold `rel_exp` 0
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN (SplitOnConclITE THENA Auto)
   THEN Reduce 0
   THEN Auto
   THEN ExRepD) }

1
1. B : Type
2. R : B ⟶ B ⟶ ℙ
3. one-one(B;B;R)
4. n : ℤ
5. 0 < n
6. one-one(B;B;R^n - 1)
7. x : B
8. ¬(n = 0 ∈ ℤ)
9. y@0 : B
10. z : B
11. z1 : B
12. x R z1
13. z1 R^n - 1 y@0
14. z@0 : B
15. x R z@0
16. z@0 R^n - 1 z
⊢ y@0 = z ∈ B

---

Latex:

---

Latex:
\mforall{}[B:Type].  \mforall{}[R:B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}].    \mforall{}[n:\mBbbN{}].  one-one(B;B;rel\_exp(B;  R;  n))  supposing  one-one(B;B;R)


By

---

Latex:
(InductionOnNat
  THEN  (D  0  THENA  Auto)
  THEN  RecUnfold  `rel\_exp`  0
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index