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