let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in
(constr_obj, constr_rel, constr_sort)
| _ -> raise NotAnInductiveDefinition
let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in
(constr_obj, constr_rel, constr_sort)
| _ -> raise NotAnInductiveDefinition