$P\; =$\%L \%a <= F[\%a].\%l( self: \%a).{ ... }
   $C\; =$\%L \%a <= G[\%a].\%l( self:\%a).P[\%a]( self ) \with { ... }
  

with recursive types
$F[\%a]\; =\; \{\; i:int,\; id:\%a\; ->\; bool\; \}$
$G[\%a]\; =\; \{\; i:int,\; id:\%a\; ->\; bool,\; b\; :\; bool\; \}$
Valid, because
However