Step
*
1
1
1
2
1
1
1
of Lemma
Q-R-glues-trivial-split
1. B : Type
2. v : bag(B)@i
⊢ (¬↑(#(v) =z 1))
⇒ (#(v) ≤ 1)
⇒ (v = {} ∈ bag(B))
BY
{ (RW assert_pushdownC 0 THEN Auto) }
1
1. B : Type
2. v : bag(B)@i
3. #(v) ≠ 1@i
4. #(v) ≤ 1@i
⊢ v = {} ∈ bag(B)
Latex:
Latex:
1. B : Type
2. v : bag(B)@i
\mvdash{} (\mneg{}\muparrow{}(\#(v) =\msubz{} 1)) {}\mRightarrow{} (\#(v) \mleq{} 1) {}\mRightarrow{} (v = \{\})
By
Latex:
(RW assert\_pushdownC 0 THEN Auto)
Home
Index