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

At: mapoutl member 2
1. A: Type
2. B: Type
3. s: (A+B) List
4. x: A
5. (inl(x) s)
y:A+B. (y s) & isl(y) & x = outl(y)
By:
InstConcl [inl(x)]
THEN
Reduce 0
Generated subgoals:

None

About:
listassertunioninluniverseequalandexists

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