如何从窄域到宽域证明全称量词？附相关引理验证

本文探讨如何从窄域命题推导证明宽域全称量词命题，给出如下两个引理：

lemma "(∀l k. l< i ∧ k<j⟶ (f l k))
         ⟹ (∀l. l< i⟶ (f l j))
        ⟹ (∀l k.  l<i ∧ k≤j⟶ (f l k))"
  oops

lemma "(∀l k. l<  i ∧ k<j⟶ (f l k)) ⟹
       (∀l. l< i⟶ (f l j)) ⟹ (∀k.  k<j⟶ (f i k)) ⟹ f i j
       ⟹ (∀l k.  l≤ i ∧ k≤j⟶ (f l k))"
  oops

已知全称量词修饰的两个窄域命题可证，能否据此证明对应的宽域命题？

内容的提问来源于stack exchange，提问作者hahahahaha-sh