(2steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: no repeats inj 1
1. T: Type
2. s: T List
3. i,j:. i < ||s|| j < ||s|| i = j s[i] = s[j]
4. a1: ||s||
5. a2: ||s||
6. s[a1] = s[a2]
7. a1 = a2
a1 = a2
By: InstHyp [a1;a2] -5
Generated subgoals:

None

About:
listnatural_numberless_thanuniverseequalimpliesall

(2steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc