************************************************************
Week 7: Proof of Exercise 7.3. Casenil Part (Induction Base)
************************************************************







Signatures::


    app  : _a list -> _a list -> _a list ;
  
	
	
	
	
	
	

Definitions::


    [app nil] : forall xs : _a list .
                app [] xs = xs : _a list ;
    [app xs]  : forall xs : _a list . forall x : _a . forall ys : _a list .
                app (x::xs) ys = x :: app xs ys : _a list ;
    







Theorem [Lemma]:: 

    Statement: forall xs: _a list . forall ys : _a list . forall zs: _a list . 
    app (app xs ys) zs = app xs (app ys zs)	: _a list 
	Proof: 
	by induction on list: 
	
	
	case nil: 
	    assume ys : _a list . 
		assume zs : _a list . 
		we know [prem 1] : app [] ys = ys : _a list 
		   because [app nil] with (ys).
		   
		we know [prem 2] : app [] (app ys zs) = (app ys zs) : _a list
           because [app nil] with (app ys zs). 
		   
        we know [step 1] : app (app [] ys) zs = app ys zs : _a list 
	       because equality on ([prem 1]).
   
        we know [step 2] : app (app [] ys) zs = app [] (app ys zs): _a list 
           because equality on ([step 1];[prem 2]). 
		   
		by [step 2]   
		
	case (x::xs) : [IH] . 
        TODO 
    QED.