Nuprl - Pf apply_alist

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

T:Type, as:(LabelT) List, d1,d2:T, x:Label. (x 1of(unzip(as))) apply_alist(as;x;d1) = apply_alist(as;x;d2)

By: Analyze 0 THEN Analyze 0 THEN ListInd -1

Generated subgoals:

1 1. T: Type
2. as: (LabelT) List
d1,d2:T, x:Label. (x 1of(unzip(nil))) apply_alist(nil;x;d1) = apply_alist(nil;x;d2)

2 1. T: Type
2. as: (LabelT) List
3. u: LabelT
4. v: (LabelT) List
5. d1,d2:T, x:Label. (x 1of(unzip(v))) apply_alist(v;x;d1) = apply_alist(v;x;d2)
d1,d2:T, x:Label. (x 1of(unzip([u / v]))) apply_alist([u / v];x;d1) = apply_alist([u / v];x;d2)

About:

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

1	1. `T:` `Type` 2. `as:` `(LabelT) List` `d1,d2:T, x:Label. (x 1of(unzip(nil))) apply_alist(nil;x;d1) = apply_alist(nil;x;d2)`
2	1. `T:` `Type` 2. `as:` `(LabelT) List` 3. `u:` `LabelT` 4. `v:` `(LabelT) List` 5. `d1,d2:T, x:Label. (x 1of(unzip(v))) apply_alist(v;x;d1) = apply_alist(v;x;d2)` `d1,d2:T, x:Label. (x 1of(unzip([u / v]))) apply_alist([u / v];x;d1) = apply_alist([u / v];x;d2)`