inductive sum (n:nat) : nat \to nat \to Set \def
k: \forall x,y. n = x + y \to sum n x y.
-theorem t: \forall x,y. \forall H: sum x y O.
+theorem t': \forall x,y. \forall H: sum x y O.
match H with [ (k a b p) \Rightarrow a ] = x.
intros.
cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x).