proposition: Lemma iota_spec_1 : unique P (iota inhA P).
proof: Proof. generalize (iota_spec inhA P unique_P). destruct unique_P as [x H]; intro H0;split;auto. intros x' Hx'; destruct H; transitivity x; auto. now rewrite (H1 _ H0). Qed.