Duck Proof Script Inductive Properties of Lists, Part 1

 ```*** file: /net/cs/htdocs/users/goguen/kumo/revlist/list0.duck ***************************************** style: beijing ***************************************** spec: /net/cs/htdocs/users/goguen/kumo/revlist/list.bob ***************************************** proof: <> goal: (forall L1 : List) rev(rev(L1)) = L1 . by: induction on L1 with scheme {nil, cons}; [] ***************************************** proof: <> goal: (forall L1 L2 : List) rev(append(L1, L2)) = append(rev(L2), rev(L1)) . by: induction on L1 with scheme {nil, cons}; [] ***************************************** proof: <> goal: (forall L1 L2 L3 : List) append(append(L1, L2), L3) = append(L1, append(L2, L3)) . by: induction on L1 with scheme {nil, cons}; [] ***************************************** display: <> dir: /net/cs/htdocs/groups/tatami/kumo/exs/list0 title: "Inductive Properties of Lists, Part 1" homepage: /net/cs/htdocs/users/goguen/kumo/revlist/list0.hp specexpl: /net/cs/htdocs/users/goguen/kumo/revlist/list.specexpl closing: /net/cs/htdocs/users/goguen/kumo/revlist/list0.close <> subtitle: "The Doubly Reversed List Equation" expl: /net/cs/htdocs/users/goguen/kumo/revlist/list0.exp1 <> subtitle: "Reverse Append Lemma" expl: /net/cs/htdocs/users/goguen/kumo/revlist/list0.exp2 <> subtitle: "Associativity of Append" expl: /net/cs/htdocs/users/goguen/kumo/revlist/list0.exp3 [] ```