-CoInductive Fresh A T :=
-{ next : forall a:A, (T a * Fresh A T)
-; split : Fresh A T * Fresh A T
-}.
+Fixpoint mfresh (f:Fresh Kind (fun _ => WeakTypeVar))(lk:list Kind){Γ}(ite:IList _ (fun _ => WeakTypeVar) Γ)
+ : (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length lk)) * (IList _ (fun _ => WeakTypeVar) (app lk Γ))) :=
+ match lk as LK return (Fresh Kind (fun _ => WeakTypeVar)) * ((vec WeakTypeVar (length LK)) *
+ (IList _ (fun _ => WeakTypeVar) (app LK Γ))) with
+ | nil => (f,(vec_nil,ite))
+ | k::lk' =>
+ let (f',varsite') := mfresh f lk' ite
+ in let (vars,ite') := varsite'
+ in let (v,f'') := next _ _ f' k
+ in (f'',((v:::vars),v::::ite'))
+ end.