2. P : A
AProp
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)
8. i :
9. i<||X @ [b; a / Y]||
10.
i<||X||
11.
i = ||X||
12. i = ||X||+1
(X @ [b; a / Y])[(||X||+1)] = (X @ [a; b / Y])[((||X||, ||X||+1)(||X||+1))]AProp
i<||X||
i = ||X||
(X @ [b; a / Y])[(||X||+1)] = (X @ [a; b / Y])[((||X||, ||X||+1)(||X||+1))]| By: |
THEN Try (Unfold `flip` 0 THEN Reduce 0 THEN Repeat SplitOnConclITE) |
| 1 |
(X @ [b; a / Y])[(||X||+1)] = (X @ [a; b / Y])[||X||] | 2 steps |
About:
 |  |  |  |  |  |  |  |  |  |  |  |