---

Step * 1 1 1 of Lemma decidable__equal_function


1. T : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. i : ℤ
4. j : ℤ
5. (j - i) ≤ 0
6. f : {i..j-} ⟶ T
7. g : {i..j-} ⟶ T
8. x : {i..j-}
⊢ (f x) = (g x) ∈ T
BY
{ TACTIC:(D -1 THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  i  :  \mBbbZ{}
4.  j  :  \mBbbZ{}
5.  (j  -  i)  \mleq{}  0
6.  f  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  T
7.  g  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  T
8.  x  :  \{i..j\msupminus{}\}
\mvdash{}  (f  x)  =  (g  x)


By

---

Latex:
TACTIC:(D  -1  THEN  Auto')

---

Home Index