proposition: Lemma Y_if_not : forall (P : Prop) (hyp : ~ P) (x y z : E), y = z -> Y P x z = y.
proof: Proof. ir. unfold Y in |- *. set (a := fun p : P => x). set (b := fun p : ~ P => z). transitivity (b hyp). ap by_cases_if_not. rewrite H. tv. Qed.
imports: tactics