+++ /dev/null
-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.