Step
*
2
of Lemma
deq-sub-bag_wf
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
⊢ case TERMOF{decidable__sub-bag:o, \\v:l, i:l} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff ∈ 𝔹
BY
{ TACTIC:(GenConclAtAddr [2;1;1] THEN Thin (-1))⋅ }
1
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
5. v : ∀bs:bag(T). Dec(sub-bag(T;as;bs))@i
⊢ case v bs of inl(x) => tt | inr(x) => ff ∈ 𝔹
Latex:
Latex:
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. bs : bag(T)
\mvdash{} case TERMOF\{decidable\_\_sub-bag:o, \mbackslash{}\mbackslash{}v:l, i:l\} deq-witness(eq) as bs of inl(x) => tt | inr(x) => ff
\mmember{} \mBbbB{}
By
Latex:
TACTIC:(GenConclAtAddr [2;1;1] THEN Thin (-1))\mcdot{}
Home
Index