DEFINITION THeads() TYPE = K→TList→T→T BODY =FIXTHeads{ THeads:K→TList→T→T :=λk:K .λus:TList .λt:T .<λt1:TList.T> CASE us OF TNil⇒t | TCons u ul⇒THead k u (THeads k ul t) }