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

At: mapoutl is singleton 1 2 2
1. A: Type
2. B: Type
3. L: (A+B) List
4. a: A
5. 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
By:
ExRepD
THEN
InstConcl [[inr(y) / L1];L2]
THEN
All Reduce
THEN
Analyze
Generated subgoals:

None

About:
listconsconsnilunioninlinruniverseequalandexists

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