(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

At: no repeats append iff 2
1. T: Type
2. l1: T List
3. l2: T List
4. i,j:. i < ||l1 @ l2|| j < ||l1 @ l2|| i = j (l1 @ l2)[i] = (l1 @ l2)[j]
5. i:
6. j:
7. i < ||l1||
8. j < ||l1||
9. i = j
l1[i] = l1[j]
By:
RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| 4
THEN
InstHyp [i;j] 4
THEN
RWO Thm* as,bs:T List, i:||as||. (as @ bs)[i] = as[i] -1
Generated subgoals:

None

About:
listintnatural_numberaddless_thanuniverseequalimpliesall

(13steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc