%%% Assignment 10
%%% Out: Mon 3 Dec
%%% Due: Mon 10 Dec 
%
% This assignment is to be submitted on paper.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 1. Structural Induction on Lists.
%
% Prove the following propositions using structural induction.
% In each case, give an informal proof and then a proof term.
% You may make use of lemmas already proved.
%
% A. !l: t-list .!k: t-list . l = k => k = l
%
% B.  !k: t-list .!l: t-list . !m: t-list .
%        rev (rev k l) m = rev l (app k m)
%  
%
% 2. Generalizing the Induction Hypothesis.
%
% Using previously proved problems and lemmas,
% give a formal proof of the following:
%
%  !l: t-list . reverse(reverse l) = l .
%
%
% 3. Dependent Types.
%
% [to be posted Wednesday 5 December]
%
%
%
%%%