Require Export Xml.

Section prova.

Inductive
 tree : Set := node : forest -> tree
with
 forest : Set := leaf : forest | cons : tree -> forest -> forest.

Fixpoint tree_size [t:tree] : nat :=
 Cases t of (node f) => (S (forest_size f)) end
with forest_size [f:forest] : nat :=
 Cases f of leaf => (S O) | (cons t f') => (plus (tree_size t) (forest_size f'))
 end.

Theorem a_ab_b: (A,B:Prop)A->(A->B)->B.
Auto.
Qed.

Axiom dummy_axiom: (n,m:nat)(le n m)\/(gt n m).

End prova.

Print XML Section Disk "examples/prove" prova.

Theorem ab_ac_abc: (A,B,C:Prop)(A->B)->(A->C)->A->B/\C.
Intros A B C AB AC A1.
Split.

Show XML File "examples/ab_ac_abc.xml" Proof.

Auto.
Auto.
Qed.