Require Export Xml.

Section a.
 Variable A:Prop.
 Section b1.
  Variable B:Prop.
  Axiom axiom: A -> (A -> B) ->B.
  Theorem th1: A -> (A -> B) -> A/\B.
   Intros A' H.
   Split.
   Assumption.
   Apply axiom; Assumption.
  Qed.
 End b1.
 Section b2.
  Variable B:Set.
  Axiom axiom': (A:Prop)A->A.
 End b2.
 Theorem th1': (A:Prop)A->A.
  Auto.
 Qed.
End a.