Given:

            data Tree a = Tip | Node a (Tree a) (Tree a)
            
            mirror Tip = Tip
            mirror (Node a l r) = Node a (mirror r) (mirror l)
            
            flatten Tip = []
            flatten (Node a l r) = flatten l ++ [a] ++ flatten r
            
            reverse [] = []
            reverse (x:xs) = reverse xs ++ [x]
            
            [] ++ ys = ys
            (x:xs) ++ ys = x : (xs ++ ys)

prove that:

            flatten . mirror = reverse . flatten
    
This is:    for all t :: Tree a, 
    
                flatten (mirror t) = reverse (flatten t)       { by function equality }
            
    Proof by induction on structure of t :: Tree a
    
        case t = Tip:
        
            flatten (mirror Tip) = reverse (flatten Tip)       { goal with t := Tip }
            
            flatten Tip = ...                                  { LHS: defn mirror }
            
            [] = ...                                           { LHS: defn flatten }
            
            [] = reverse (flatten Tip)                         { reiterate RHS }
            
            [] = reverse []                                    { RHS: defn flatten }
            
            [] = []                                            { RHS: defn reverse }
            
            QED                                                { reflexivity of equality }
    
        case t = Node a l r:
        
            flatten (mirror (Node a l r)) = reverse (flatten (Node a l r))
            
                                                                { goal with t := Node a l r }
        
            flatten (Node a (mirror r) (mirror l)) = ...
            
                                                                { LHS: defn mirror }
        
            flatten (mirror r) ++ [a] ++ flatten (mirror l) = ...
            
                                                                { LHS: defn flatten }
        
            flatten (mirror r) ++ ([a] ++ flatten (mirror l)) = ...
            
                                                                { clarify: ++ associates right }
        
            ... = reverse (flatten (Node a l r))                { reiterate RHS }
        
            ... = reverse (flatten l ++ [a] ++ flatten r)       { RHS: defn flatten }
        
            ... = reverse (flatten l ++ ([a] ++ flatten r))     { clarify: ++ associates right }
        
            ... = reverse ([a] ++ flatten r) ++ reverse (flatten l)
            
                                                                { lemma 1: see below }
        
            ... = (reverse (flatten r) ++ reverse [a]) ++ reverse (flatten l)
            
                                                                { lemma 1: see below }
        
            ... = reverse (flatten r) ++ (reverse [a] ++ reverse (flatten l))
            
                                                                { lemma 2: see below }
        
            ... = reverse (flatten r) ++ ([a] ++ reverse (flatten l))
            
                                                                { lemma 3: see below }
        
            flatten (mirror r) ++ ([a] ++ flatten (mirror l)) = 
            reverse (flatten r) ++ ([a] ++ reverse (flatten l))
            
                                                                { reiterate LHS }
        
            reverse (flatten r) ++ ([a] ++ flatten (mirror l)) = 
            reverse (flatten r) ++ ([a] ++ reverse (flatten l))
            
                                                                { subn, ind. hyp. on r }
        
            reverse (flatten r) ++ ([a] ++ reverse (flatten l)) = 
            reverse (flatten r) ++ ([a] ++ reverse (flatten l))
            
                                                                { subn, ind. hyp. on l }
        
            QED                                                 { reflexivity of equality }

Lemma 1:    

    for all xs, ys :: [a],

        reverse (xs ++ ys) = reverse ys ++ reverse xs
            
    Proof by induction on structure of xs :: [a]
    
        case xs = []:
        
            reverse ([] ++ ys) = reverse ys ++ reverse []          { goal with xs := [] }
        
            reverse ys = reverse ys ++ reverse []                  { defn ++ }
        
            reverse ys = reverse ys ++ []                          { defn reverse }
        
            reverse ys = reverse ys                                { lemma 1.5, see below }
        
            QED                                                    { reflexivity of equality }
    
        case xs = (a:as):
        
            reverse ((a:as) ++ ys) = reverse ys ++ reverse (a:as)      
                                                                   { goal with xs := a : as }
        
            reverse (a : (as ++ ys)) = ...                         { LHS, defn of ++ }
        
            reverse (as ++ ys) ++ [a] = ...                        { LHS, defn of reverse }
        
            ... = reverse ys ++ reverse (a:as)                     { reiterate RHS }
        
            ... = reverse ys ++ (reverse as ++ [a])                { RHS, defn reverse }
        
            reverse (as ++ ys) ++ [a] = (reverse ys ++ reverse as) ++ [a]          
                                                                    { reiterate LHS }
        
            reverse (as ++ ys) = (reverse ys ++ reverse as)        { focus from context }
        
            reverse (as ++ ys) = reverse (as ++ ys)                { ind. hyp. on as, ys }
        
            QED                                                    { reflexivity of equality }


Lemma 1.5:  

    for all xs :: [a],

        xs ++ [] = xs
            
    Proof by induction on structure of xs :: [a]
    
        case xs = []:
        
            [] ++ [] = []                                      { goal with xs := [] }
        
            [] = []                                            { defn ++ }
        
            QED                                                { reflexivity of equality }
    
        case xs = (y:ys):
        
            (y : ys) ++ [] = y : ys                            { goal with xs := y : ys }
        
            y : (ys ++ []) = y : ys                            { defn ++ }
        
            y : ys = y : ys                                    { ind hyp on ys }
        
            QED                                                { reflexivity of equality }


Lemma 2: 

    for all xs, ys, zs :: [a],

        (xs ++ ys) ++ zs = xs ++ (ys ++ zs)
            
    Proof by induction on structure of xs :: [a]
    
        case xs = []:
        
            ([] ++ ys) ++ zs = [] ++ (ys ++ zs)                { goal with xs := [] }
        
            ys ++ zs = [] ++ (ys ++ zs)                        { defn ++, LHS }
        
            ys ++ zs = ys ++ zs                                { defn ++, RHS }
        
            QED                                                { reflexivity of equality }
    
        case xs = (a:as):
        
            ((a:as) ++ ys) ++ zs = (a:as) ++ (ys ++ zs)        { goal with xs := a : as }
        
            (a : (as ++ ys)) ++ zs = (a:as) ++ (ys ++ zs)      { defn ++, LHS }
        
            (a : (as ++ ys)) ++ zs = a : (as ++ (ys ++ zs))    { defn ++, RHS }
        
            a : ((as ++ ys) ++ zs) = a : (as ++ (ys ++ zs))    { lemma 2.5, LHS, see below }
        
            a : (as ++ (ys ++ zs)) = a : (as ++ (ys ++ zs))    { lemma 2.5, ind. hyp. on as }
        
            QED                                                { reflexivity of equality }


Lemma 2.5: 

    for all a :: a, xs, ys :: [a],

        (a : xs) ++ ys = a : (xs ++ ys)
            
    Proof by induction on structure of xs :: [a]
    
        case xs = []:
        
            (a : []) ++ ys = a : ([] ++ ys)                { goal with xs := [] }
        
            a : ([] ++ ys) = a : ([] ++ ys)                { defn ++, LHS }
        
            QED                                             { reflexivity of equality }
    
        case xs = (a:as):
        
            (a : as) ++ ys = a : (xs ++ ys)                { goal with xs := a : as }
        
            a : (as ++ ys) = a : (xs ++ ys)                { LHS, defn ++ }
        
            QED                                            { reflexivity of equality }


Lemma 3: 

    for all a :: a,

        reverse [a] = [a]                              { original goal }

        reverse (a : []) = [a]                         { list notation, twice }

        reverse [] ++ [a] = [a]                        { defn reverse }

        [] ++ [a] = [a]                                { defn reverse }

        [a] = [a]                                      { defn ++ }

        QED                                            { reflexivity of equality }