helm/EXPORT/exportprove/prove/provastruct.v

   1 Require Export Xml.
   2
   3 Section a.
   4  Variable A:Prop.
   5  Section b1.
   6   Variable B:Prop.
   7   Axiom axiom: A -> (A -> B) ->B.
   8   Theorem th1: A -> (A -> B) -> A/\B.
   9    Intros A' H.
  10    Split.
  11    Assumption.
  12    Apply axiom; Assumption.
  13   Qed.
  14  End b1.
  15  Section b2.
  16   Variable B:Set.
  17   Axiom axiom': (A:Prop)A->A.
  18  End b2.
  19  Theorem th1': (A:Prop)A->A.
  20   Auto.
  21  Qed.
  22 End a.