% Leo-III cross-check.
% Proof (a), part 1 -- Ibn Sina's case split: since something exists, it is necessary
% (done) or possible; the possible case is part 2 (supplied as proved there and in Rocq:
% ImkanConclusion.necessary_existent_from_a_possible).
% Vocabulary.  Nothing is assumed about these symbols.
thf(ex_type, type, ex: $i > $o).                     % (ex @ X): X exists
thf(ess_type, type, ess: $i > $o).                   % (ess @ X): X's existence is from its nature
thf(gives_type, type, gives: $i > $i > $o).          % (gives @ Y @ X): Y gives existence to X
thf(nec_type, type, nec: $i > $o).
thf(poss_type, type, poss: $i > $o).
thf(ta_type, type, through_another: $i > $o).
thf(nec_def, definition, nec = (^[X:$i]: ((ex @ X) & (ess @ X)))).            % necessary in itself
thf(poss_def, definition, poss = (^[X:$i]: ((ex @ X) & ~ (ess @ X)))).        % possible in itself
thf(ta_def, definition, through_another = (^[X:$i]: ?[Y:$i]: (gives @ Y @ X))). % something gives X existence
thf(mem_type, type, mem: $i > $i > $o).              % (mem @ P @ A): P is a member of collection A
thf(agg_type, type, agg: $i > $o).
thf(agg_def, definition, agg = (^[A:$i]: ((![P:$i]: ((P != A) => ((mem @ P @ A) <=> (poss @ P)))) & ~ (mem @ A @ A)))).
thf(step1, axiom, ![X:$i]: ((ex @ X) => ((nec @ X) | (poss @ X)))).                    % PR-006 division_exhaustive
thf(possible_case, axiom, (?[P:$i]: (poss @ P)) => (?[N:$i]: (nec @ N))).               % parts 2a and 2b; Rocq necessary_existent_from_a_possible
thf(sp001, axiom, ?[X:$i]: (ex @ X)).                                                % SP-001
thf(conclusion, conjecture, ?[N:$i]: (nec @ N)).