<div dir="ltr">Hi,<div><br></div><div>In the following the _ in &quot;yellow&quot; is not resolved while the one in &quot;inferred&quot; is.</div><div>Is it because g is not invariant in that argument and so it matters what we pass to it?</div>
<div><br></div><div><div>open import Relation.Binary.PropositionalEquality</div><div><br></div><div>data X : Set where</div><div>  x : X</div><div><br></div><div>f : X -&gt; X -&gt; Set</div><div>f _ x = X</div><div><br></div>
<div>postulate</div><div>  stuck : X</div><div>  g : ∀ z -&gt; f z stuck</div><div><br></div><div>yellow : ∀ z -&gt; f z stuck</div><div>yellow z = g _</div><div>              </div><div>inferred : ∀ z -&gt; f _ ≡ f z</div>
<div>inferred z = refl</div></div><div><br></div><div><br></div><div>-- Andrea</div></div>