Step
*
1
1
1
1
of Lemma
primed-class-prior-val
.....equality.....
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
7. x : E@i
8. (x <loc e)@i
9. ↑0 <z #(X es x)@i
10. ∀e'':E. ((x <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))@i
11. x1 : E@i
12. (x1 <loc e)@i
13. ↑(#(X es x1) =z 1)@i
14. ∀e'':E. ((x1 <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(#(X es e'') =z 1)))@i
⊢ x = x1 ∈ E
BY
{ ((InstLemma `es-locl-total` [⌈es⌉;⌈x⌉;⌈x1⌉]⋅ THENA Auto) THEN SplitOrHyps THEN Auto) }
1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
7. x : E@i
8. (x <loc e)@i
9. ↑0 <z #(X es x)@i
10. ∀e'':E. ((x <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))@i
11. x1 : E@i
12. (x1 <loc e)@i
13. ↑(#(X es x1) =z 1)@i
14. ∀e'':E. ((x1 <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(#(X es e'') =z 1)))@i
15. (x <loc x1)
⊢ x = x1 ∈ E
2
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
7. x : E@i
8. (x <loc e)@i
9. ↑0 <z #(X es x)@i
10. ∀e'':E. ((x <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))@i
11. x1 : E@i
12. (x1 <loc e)@i
13. ↑(#(X es x1) =z 1)@i
14. ∀e'':E. ((x1 <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑(#(X es e'') =z 1)))@i
15. (x1 <loc x)
⊢ x = x1 ∈ E
Latex:
Latex:
.....equality.....
1. Info : Type
2. T : Type
3. X : EClass(T)
4. Singlevalued(X)
5. es : EO+(Info)
6. e : E
7. x : E@i
8. (x <loc e)@i
9. \muparrow{}0 <z \#(X es x)@i
10. \mforall{}e'':E. ((x <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}0 <z \#(X es e'')))@i
11. x1 : E@i
12. (x1 <loc e)@i
13. \muparrow{}(\#(X es x1) =\msubz{} 1)@i
14. \mforall{}e'':E. ((x1 <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(\#(X es e'') =\msubz{} 1)))@i
\mvdash{} x = x1
By
Latex:
((InstLemma `es-locl-total` [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]\mcdot{} THENA Auto) THEN SplitOrHyps THEN Auto)
Home
Index