%------------------------------------------------------------------------------
thf(bird_type,type,( bird: $tType )).
thf(tweety_type,type,( tweety: bird )).

thf(list_type,type,( list: $tType > $tType )).
thf(map_type,type,( map: $tType > $tType > $tType )).

thf(bird_lookup_type,type,(
    bird_lookup: !>[A: $tType,B: $tType] : ( ( map @ A @ B ) > A > B ) )).
thf(bird_update_type,type,(
    bird_update: !>[A: $tType,B: $tType] :
                   ( ( map @ A @ B ) > A > B > ( map @ A @ B ) ) )).
thf(idempotent_type,type,( idempotent: !>[A: $tType] : ( ( A > A ) > $o ) )).

thf(bird_lookup_update_same,axiom,(
    ! [RangeType: $tType,Map: ( map @ bird @ RangeType ),
       Key: bird,Value: RangeType] :
      ( ( bird_lookup @ bird @ RangeType @ 
          ( bird_update @ bird @ RangeType @ Map @ Key @ Value ) @ Key )
      = Value ) )).

thf(idempotent_def,definition,(
    ! [A: $tType,F: ( A > A )] :
      ( ( idempotent @ A @ F )
      = ( ! [X: A] : ( ( F @ ( F @ X ) ) = ( F @ X ) ) ) ) )).

thf(higher_order_conjecture,conjecture,(
    ! [Value: ( list @ $i )] :
      ( idempotent @ ( map @ bird @ ( list @ $i ) )
      @ ^ [Map: ( map @ bird @ ( list @ $i ) )] :
          ( bird_update @ bird @ ( list @ $i ) @ Map @ tweety @ Value ) ) )).
%------------------------------------------------------------------------------