]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prove/provastruct5.v
...
[helm.git] / helm / EXPORT / exportprove / prove / provastruct5.v
1 Section a.
2  Variable A:Prop.
3  Theorem easy:(B:Prop)B->B.
4   Exact ([H:Prop][B:Prop][b:B]b A).
5  Qed.
6  Section b.
7   Theorem easy':(B:Prop)B->B.
8    Exact easy.
9   Qed.
10  End b.
11 End a.