全称記号の使い方と内部変形

variable (α : Type)
variable (F G : α → Type)
def f : (∀ x : α, F x × G x) → (∀ y : α, F y) :=
  fun h : ∀ x : α, F x × G x =>
  fun y : α => (h y).fst

関数ヘッドを変形すると：

variable (α : Type)
variable (F G : α → Type)
def f' (h : ∀ x : α, F x × G x) : (∀ y : α, F y) :=
 fun y : α => (h y).fst

variableの包摂〈取り込み〉すると：

def f'' (α : Type) (F G : α → Type) (h : ∀ x : α, F x × G x) : (∀ y : α, F y) :=
 fun y : α => (h y).fst

圏論的プロファイル形式を書くと：

f'' :
 (α : Type), (F G : α → Type), (h : ∀ x : α, F x × G x) 
 |- (∀ y : α, F y)

内部的に次のように変形される。

f'' :
 (α : Type), (F G : α → Type), (h : (x : α) → F x × G x) 
 |- (y : α) → F y