一阶直觉主义逻辑中该形式引理是否成立？

对应的Coq一阶引理代码如下：

Lemma nop_firstorder :
     forall (n n1 n2:nat) (input: list nat),
          ( (exists p : prog, isValidProg p input -> execProg p [] input = Some [n;n1;n2]) ->
              (exists p : prog, isValidProg p input -> execProg p [] input = Some [n]) ) ->
          ( (forall p : prog, isValidProg p input -> execProg p [] input <> Some [n]) ->
              (forall p : prog, isValidProg p input -> execProg p [] input <> Some [n;n1;n2]) ).

这个引理在一阶直觉主义逻辑中为假，无法被firstorder策略证明和搜索深度设置无关，核心问题是引理的前提表述和直觉语义不一致，在直觉主义框架下前提过弱，无法支撑结论：

• 前提中的exists p : prog, isValidProg p input -> execProg p [] input = Some [n;n1;n2]是极容易满足的命题。根据直觉主义逻辑对蕴含的解释，只要存在任意一个程序p使得isValidProg p input不成立，这个蕴含式就自动为真（蕴含前件为假时整个式子成立），完全不需要真的存在合法程序执行后得到[n;n1;n2]的结果。
• 前提里的后件exists p : prog, isValidProg p input -> execProg p [] input = Some [n]同理，只要存在一个非法程序p，这个存在命题就成立。也就是说整个大前提只要prog类型非空、存在至少一个不满足isValidProg判定的程序，就会自动成立，根本没有对合法程序的实际执行结果做出任何有效约束。
• 在这个前提下，结论完全可能不成立：可以构造出满足大前提的模型（靠存在非法程序让两个存在命题都为真），同时满足“所有合法程序都得不到结果[n]”，但存在某合法程序能得到结果[n;n1;n2]，此时结论直接为假。
• 该命题在经典逻辑中看似为真，本质是下意识把前提里的exists p, (A p -> B p)等价成了(exists p, A p /\ B p) -> (exists p, A p /\ B' p)——后者才是真正想表达的“如果存在合法程序跑出三元结果，就存在合法程序跑出一元结果”的语义，而当前写法的前提比这个语义弱得多，二者在直觉主义逻辑中完全不等价。

内容的提问来源于stack exchange，提问作者FH35