let mk_exists ooch noch c v =
let description = "multiple existental quantifier" in
let prec = "non associative with precedence 20\n" in
let mk_exists ooch noch c v =
let description = "multiple existental quantifier" in
let prec = "non associative with precedence 20\n" in
let ele n = P.sprintf "x%u" (v - n) in
let ele_list = string_iter "," ele v in
let ele_seq = string_iter " " ele v in
let ele n = P.sprintf "x%u" (v - n) in
let ele_list = string_iter "," ele v in
let ele_seq = string_iter " " ele v in
let abst b n = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in
P.sprintf "λ${ident x%u}%s" (v - n) xty in
let abst b n = let xty = if b then P.sprintf ":$T%u" (v - n) else "" in
P.sprintf "λ${ident x%u}%s" (v - n) xty in
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;