Nuprl - Proof: l before-iff 2 1 1 1

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

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. x,y:T. x before y v (L1,L2,L3:T List. v = (L1 @ [x] @ L2 @ [y] @ L3))
6. x: T
7. y: T
8. x = u
9. (y v)

L1,L2,L3:T List. [u / v] = (L1 @ [x] @ L2 @ [y] @ L3)

By: Inst Thm* s:T List, z:T. (z s) (s1,s2:T List. s = (s1 @ [z / s2])) [T;v;y] THEN ExRepD THEN InstConcl [nil;s1;s2] THEN Reduce 0

Generated subgoal:

1 10. s1: T List
11. s2: T List
12. v = (s1 @ [y / s2])
[u / v] = [x / (s1 @ [y / s2])] 1 step

About:

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