Section a.
 Variables N,M:nat.
 Section b.
  Variable P:Prop.
  Local SN := (S N).
  Axiom A : N = M.
 End b.
End a.