1theory Util
2  imports Main
3begin
4
5lemma prod_split_asmE: 
6  "\<lbrakk> (a,b) = x; P (fst x) (snd x) \<rbrakk> \<Longrightarrow> P a b"
7  by (clarsimp split: prod.split)
8
9lemma prod_eq: 
10  "\<lbrakk> a = fst x ; b = snd x \<rbrakk> \<Longrightarrow> x = (a,b)"
11  by simp
12
13end