Inductive MS: Set := X:MS->MS | Y:MS->MS.
 
Type  [p:MS]<nat>Cases p of (X x) => O end.