]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prove/provastruct.v
...
[helm.git] / 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.