ocaml 3.09 transition

[helm.git] / helm / EXPORT / exportprove / prove / provastruct4.v

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