Initial subsumption definitions for match and Isabelle/HOL proof that they form a semi-lattice.