and 'term arg =
Aux of string
| Premise of premise
+ | Lemma of lemma
| Term of 'term
| ArgProof of 'term proof
| ArgMethod of string (* ???? *)
premise_binder : string option;
premise_n : int option;
}
+
+and lemma =
+ { lemma_id: string;
+ lemma_name: string;
+ lemma_uri: string
+ }
+
;;
type 'term conjecture = id * int * 'term context * 'term