IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
swap cons2112 1. T : Type
2. L : T List
3. x : T 4. i : {1..(||L||+1)}
5. j : {1..(||L||+1)}
6. i1 : 7. i1<||swap([x / L];i;j)||
8. i1 = 0
[x / L][((i, j)(0))] = x
By:
Subst' ((i, j)(0) = 0) 0 THEN Reduce 0 THEN Unfold `flip` 0 THEN Reduce 0
THEN
Repeat SplitOnConclITE
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
[x / L][((i, j)(0))] = x
