can-unify := λ(: fpt List<Type>)(: pt List<Type>). (: (
   (let r 0_u64)
   (match (Tuple( fpt pt )) (
      ()
      ( (Tuple( LEOF LEOF )) (set r 1_u64) )
      ( (Tuple( (LCons( lp1 lpr )) (LCons( rp1 rpr )) )) (
         (if (can-unify( lp1 rp1 )) (
            (if (can-unify( lpr rpr )) (
               (set r 1_u64)
            ) ())
         ) ())
      ))
      ( _ () )
   ))
   r
) U64);

can-unify := λ(: fpt Type)(: pt Type). (: (
   (let r 0_u64)
   (match (Tuple( fpt pt )) (
      ()
      ( (Tuple( TAny _ )) (set r 1_u64) )
      ( (Tuple( (TGround( 'Meta_s _ )) _ )) (set r 1_u64) )
      ( (Tuple( (TVar( ltv )) rt )) (set r 1_u64) )
      ( (Tuple( (TAnd( lt1 lt2 )) rt )) (
         (if (can-unify( lt1 rt )) (
            (if (can-unify( lt2 rt )) (
               (set r 1_u64)
            ) ())
         ) ())
      ))
      ( (Tuple( lt (TAnd( rt1 rt2 )) )) (
         (if (can-unify( lt rt1 )) (set r 1_u64) ())
         (if (can-unify( lt rt2 )) (set r 1_u64) ())
      ))

      # Varargs
      ( (Tuple(
         (TGround( 'Cons_s (LCons(
            (TGround( '..._s (LCons( lp1 LEOF )) ))
            (LCons( lpr LEOF ))
         )) ))
         (TGround( 'Cons_s (LCons( rp1 (LCons( rpr LEOF )) )) ))
      )) (
         (if (can-unify( lp1 rp1 )) (
            (set r (can-unify( fpt rpr )))
         ) (
            (set r (can-unify( lpr pt )))
         ))
      ))
      ( (Tuple(
         (TGround( 'Cons_s (LCons(
            (TGround( '..._s (LCons( lp1 LEOF )) ))
            (LCons( lpr LEOF ))
         )) ))
         rp1
      )) (
         (if (can-unify( lp1 rp1 )) (
            (set r (can-unify( lpr (t1 'Nil_s) )))
         ) (
            (set r (can-unify( lpr rp1 )))
         ))
      ))
      ( (Tuple(
         (TGround( '..._s (LCons( lp1 LEOF )) ))
         (TGround( 'Cons_s (LCons( rp1 (LCons( rpr LEOF )) )) ))
      )) (
         (if (can-unify( lp1 rp1 )) (
            (set r (can-unify( fpt rpr )))
         ) ())
      ))
      ( (Tuple(
         (TGround( '..._s (LCons( lp1 LEOF )) ))
         (TGround( 'Nil_s LEOF ))
      )) (
         (set r 1_u64)
      ))
      ( (Tuple(
         (TGround( '..._s (LCons( lp1 LEOF )) ))
         rp1
      )) (
         (set r (can-unify( lp1 rp1 )))
      ))

      ( (Tuple( (TGround( 'GT_s (LCons( (TGround( lbase LEOF )) LEOF )) )) (TGround( rbase LEOF )) )) (
         (if (>( (to-i64 rbase) (to-i64 lbase) )) (
            (set r 1_u64)
         ) ())
      ))
      ( (Tuple( (TGround( ltn lps )) (TGround( rtn rps )) )) (
         (if (==( ltn rtn )) (
            (if (can-unify( lps rps )) (
               (set r 1_u64)
            ) ())
         ) ())
      ))
      ( _ () )
   ))
   r
) U64);