lemma all_exist:
fixes a b :: nat and c :: int*
assumes "..."*
shows "<exists> a1 a2 a3 a4 a5 a6 a7 :: int. {around 15 equations and inequalities that define the integers}*
proof -
    ...
    from s1 s2 ... sn have final: "<exists> a1 a2 a3 a4 a5 a6 a7 :: int. {all those 15 equations and inequalities that define a1 to a7}" by force
    from final show ?thesis sorry
qed