include "arithmetics/nat.ma".

record Info (A: Type[0]): Type[0] ≝
{
  UF_I_Weight: nat;
  UF_I_Descriptor: A
}.

inductive Point (A: Type[0]): Type[0] ≝
  UF_P_Link: Link A → Point A
and inductive Link (A: Type[0]): Type[0] ≝
  | UF_L_Info: Info A → Link A
  | UF_I_Link: Point A → Link A.