]> matita.cs.unibo.it Git - helm.git/blob - helm/EXPORT/exportprove/prove/provastruct3.v
* removed memory leak (maybe)
[helm.git] / helm / EXPORT / exportprove / prove / provastruct3.v
1 Section a.
2  Section a1.
3   Variable A : Prop.
4   Variable B : Prop.
5   Inductive t1 : Set := k1 : A -> t1.
6  End a1.
7  
8  Inductive t2 [B:Set] : Set := k2 : (t2 B).
9
10  Variable A : Prop.
11 End a.