Step
*
1
of Lemma
cons_neq_nil
1. T : Type
2. h : T
3. t : T List
4. [h / t] = [] ∈ (T List)
⊢ False
BY
{ (ApFunToHypEquands `xs' ⌜case xs of [] => 0 | y::ys => 1 esac⌝ ⌜ℤ⌝ 4⋅ THENA Auto) }
1
1. T : Type
2. h : T
3. t : T List
4. [h / t] = [] ∈ (T List)
5. case [h / t] of [] => 0 | y::ys => 1 esac = case [] of [] => 0 | y::ys => 1 esac ∈ ℤ
⊢ False
Latex:
Latex:
1. T : Type
2. h : T
3. t : T List
4. [h / t] = []
\mvdash{} False
By
Latex:
(ApFunToHypEquands `xs' \mkleeneopen{}case xs of [] => 0 | y::ys => 1 esac\mkleeneclose{} \mkleeneopen{}\mBbbZ{}\mkleeneclose{} 4\mcdot{} THENA Auto)
Home
Index