At:
mapoutl is singleton
1
2
1
1.
A: Type
2.
B: Type
3.
L: (A+B) List
4.
a: A
5.
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
By:
SplitCons -1
THEN
InstConcl [nil;v]
THEN
Reduce 0
THEN
Analyze
THEN
ObviousFrom [-2]
Generated subgoals:
None
About:
