proposition: Lemma tight_is_tight x y: tight y = Some x -> I x = y.
proof: Proof. unfold tight. destruct R. destruct (I x0 == y). all: try discriminate. now injection 1 as ->. Qed.
imports: Undecidability.HOU(std.misc std.decidable) FinFun