th_Gb: THEORY
 BEGIN

  PPL: TYPE = {a, b, c}

  ADR: TYPE = {x:nat | 1 <= x AND x <= 3}

  H: {fn: [PPL -> ADR] | (FORALL (x, y: PPL): fn(x) = fn(y) => x = y)}


  L1: LEMMA (FORALL (y:ADR): y= 1 OR y=2 OR y=3)
  L2: LEMMA EXISTS (p: PPL): H(p) = 1
 END th_Gb