(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc

At: apply alist non member 1
1. T: Type
2. as: (LabelT) List

d:T, x:Label. (x nil) apply_alist(nil;x;d) = d
By:
Auto
THEN
Inst Thm* d:Top, l:Label. apply_alist(nil;l;d) ~ d [d;x]
THEN
Try (Unfold `top` 0)
THEN
HypSubst -1 0
Generated subgoals:

None

About:
productlistniluniverseequalimpliesall

(9steps) PrintForm Definitions Lemmas mb automata 1 Sections GenAutomata Doc