Step
*
1
1
1
of Lemma
deq-implies
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T. (x = y ∈ T
⇐⇒ ↑(eq x y))
4. x : T
5. y : T
⊢ (x = y ∈ T
⇐⇒ ↑(eq x y)) ⟶ (eq x y ∈ x = y ∈ T + ((x = y ∈ T) ⟶ False))
BY
{ ((BoolCase ⌜eq x y⌝⋅ THENM D 0) THENA Auto) }
1
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T. (x = y ∈ T
⇐⇒ ↑(eq x y))
4. x : T
5. y : T
6. ↑(eq x y)
7. x = y ∈ T
⇐⇒ True
⊢ tt ∈ x = y ∈ T + ((x = y ∈ T) ⟶ False)
2
1. T : Type
2. eq : T ⟶ T ⟶ 𝔹
3. ∀x,y:T. (x = y ∈ T
⇐⇒ ↑(eq x y))
4. x : T
5. y : T
6. ¬↑(eq x y)
7. x = y ∈ T
⇐⇒ False
⊢ ff ∈ x = y ∈ T + ((x = y ∈ T) ⟶ False)
Latex:
Latex:
1. T : Type
2. eq : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbB{}
3. \mforall{}x,y:T. (x = y \mLeftarrow{}{}\mRightarrow{} \muparrow{}(eq x y))
4. x : T
5. y : T
\mvdash{} (x = y \mLeftarrow{}{}\mRightarrow{} \muparrow{}(eq x y)) {}\mrightarrow{} (eq x y \mmember{} x = y + ((x = y) {}\mrightarrow{} False))
By
Latex:
((BoolCase \mkleeneopen{}eq x y\mkleeneclose{}\mcdot{} THENM D 0) THENA Auto)
Home
Index