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

At: mapoutl member 1
1. A: Type
2. B: Type
3. s: (A+B) List
4. x: A
5. y:A+B. (y s) & isl(y) & x = outl(y)
(inl(x) s)
By:
ExRepD
THEN
Analyze -4
THEN
All Reduce
THEN
HypSubst -1 0
Generated subgoals:

None

About:
listassertunioninluniverseequalandexists

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