 Structural recursion

Recursion following the constructors of a finite inductive datatype. Correctness is naturally proved by structural induction.

// Target: computer-science.bigb