Our induction is on the tree t.  Base case:  t = Leaf x.

fringe (reverseTree (Leaf x))       {unfold reverseTree}
=> fringe (Leaf x)                  {unfold fringe}	 
=> [x]                              {fold reverse of singleton} 
=> reverse [x]                      {fold fringe} 
=> reverse (fringe (Leaf x))		


IH: Holds for all trees smaller than  t = Branch t1 t2, so in particular: 
  fringe (reverseTree t1) = reverse (fringe t1)
  fringe (reverseTree t2) = reverse (fringe t2)

fringe (reverseTree (Branch t1 t2))}                   {unfold reverseTree} 
=> fringe (Branch (reverseTree t2) (reverseTree t1))   {unfold fringe} 
=> fringe (reverseTree t2) ++ fringe (reverseTree t1)  {inductive hypothesis} 
=> reverse (fringe t2) ++ reverse (fringe t1)	       {fold first fact above} 
=> reverse (fringe t1 ++ fringe t2)}                   {fold fringe} 
=> reverse (fringe (Branch t1 t2)) }