finish the NoDangling constraint
finish the NoDangling constraint

note that we have an asymmetry:
 - on the value side have (Pntr (S n) ...
 - on the type side this now corresponds to Pntr n

I should fix the value side next so we can rectify this.

minad/omega,cartazio/omega