[∀ x.A]1 [∀x. (A→B)]2 ------------- (∀E) ------------------- (∀E) A A→B -------------------------------------- (→E) B ---------- (∀I) ∀x.B ----------------- (→I) (1) (∀x.A) → (∀y.B) ------------------------------------------ (→I)(2) (∀x. (A→B)) → ( (∀x.A) → (∀y.B))