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

At: mapoutl is singleton 1 2

1. A: Type
2. B: Type
3. L: (A+B) List
4. a: A
5. u: A+B
6. v: (A+B) List
7. mapoutl(v) = [a] (L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)
mapoutl([u / v]) = [a] (L1,L2:(A+B) List. [u / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil)

By:
Analyze -3
THEN
Reduce 0
THEN
ThinTrivial


Generated subgoals:

15. x: A
6. v: (A+B) List
7. mapoutl(v) = [a] (L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil)
8. [x / mapoutl(v)] = [a]
L1,L2:(A+B) List. [inl(x) / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil
1 step
 
25. y: B
6. v: (A+B) List
7. mapoutl(v) = [a]
8. L1,L2:(A+B) List. v = (L1 @ [inl(a)] @ L2) & mapoutl(L1) = nil & mapoutl(L2) = nil
L1,L2:(A+B) List. [inr(y) / v] = (L1 @ [inl(a) / L2]) & mapoutl(L1) = nil & mapoutl(L2) = nil
1 step

About:
listconsconsnilunioninl
inruniverseequalimpliesandexists

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