---

Step * 1 1 1 of Lemma es-interface-extensionality


1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
⊢ (#(v) ≤ 1)
⇒ (#(v1) ≤ 1)
⇒ ((↑(#(v) =z 1)) ⇒ (↑(#(v1) =z 1)) ⇒ (only(v) = only(v1) ∈ A))
⇒ (↑(#(v) =z 1) ⇐⇒ ↑(#(v1) =z 1))
⇒ (v = v1 ∈ bag(A))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN (AutoBoolCase ⌈(#(v) =z 1)⌉⋅ THEN AutoBoolCase ⌈(#(v1) =z 1)⌉⋅ THEN EAuto 1)) }

1
1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
4. #(v) ≤ 1@i
5. #(v1) ≤ 1@i
6. #(v) = 1 ∈ ℤ
7. #(v1) = 1 ∈ ℤ
8. True ⇐ True@i
9. True@i
10. only(v) = only(v1) ∈ A@i
⊢ v = v1 ∈ bag(A)

2
1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
4. (#(v) + 1) ≤ 1
5. #(v1) ≤ 1@i
6. #(v1) = 1 ∈ ℤ
7. False ⇒ True ⇒ (only(v) = only(v1) ∈ A)@i
8. False ⇒ True@i
9. False ⇐ True@i
⊢ v = v1 ∈ bag(A)

3
1. A : Type
2. v : bag(A)@i
3. v1 : bag(A)@i
4. (#(v) + 1) ≤ 1
5. (#(v1) + 1) ≤ 1
6. False ⇒ False ⇒ (only(v) = only(v1) ∈ A)@i
7. False ⇒ False@i
8. False ⇐ False@i
⊢ v = v1 ∈ bag(A)

---

Latex:



1.  A  :  Type
2.  v  :  bag(A)@i
3.  v1  :  bag(A)@i
\mvdash{}  (\#(v)  \mleq{}  1)
{}\mRightarrow{}  (\#(v1)  \mleq{}  1)
{}\mRightarrow{}  ((\muparrow{}(\#(v)  =\msubz{}  1))  {}\mRightarrow{}  (\muparrow{}(\#(v1)  =\msubz{}  1))  {}\mRightarrow{}  (only(v)  =  only(v1)))
{}\mRightarrow{}  (\muparrow{}(\#(v)  =\msubz{}  1)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}(\#(v1)  =\msubz{}  1))
{}\mRightarrow{}  (v  =  v1)


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (AutoBoolCase  \mkleeneopen{}(\#(v)  =\msubz{}  1)\mkleeneclose{}\mcdot{}  THEN  AutoBoolCase  \mkleeneopen{}(\#(v1)  =\msubz{}  1)\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
  )

---

Home Index