let full b n = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in
let full_seq b = string_iter " " (full b) c in
let full b n = P.sprintf "(%s.$P%u)" (abst_clo b) (c - n) in
let full_seq b = string_iter " " (full b) c in
P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n"
o_name set_list pre_list set_type;
P.fprintf ooch "inductive %s (%s:Type[0]) (%s:%s→Prop) : Prop ≝\n"
o_name set_list pre_list set_type;
o_name ele_list pre_type o_name qm_set qm_pre;
P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n"
description c v i_name pre_seq o_name qm_set pre_seq;
o_name ele_list pre_type o_name qm_set qm_pre;
P.fprintf ooch "interpretation \"%s (%u, %u)\" %s %s = (%s %s %s).\n\n"
description c v i_name pre_seq o_name qm_set pre_seq;
P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
description c i_name pre_seq o_name pre_seq;
P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
description c i_name pre_seq o_name pre_seq;
o_name pre_type o_name qm_pre;
P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
description c i_name pre_seq o_name pre_seq;
o_name pre_type o_name qm_pre;
P.fprintf ooch "interpretation \"%s (%u)\" %s %s = (%s %s).\n\n"
description c i_name pre_seq o_name pre_seq;