proposition: Lemma surj : forall i j a : E, ex (fun b : E => create i j b = a).
proof: Proof. ir. apply by_cases with (a = i). ir. apply ex_intro with j. rewrite H. ap i_j_j. ir. apply by_cases with (a = j). ir. apply ex_intro with i. rewrite H0. ap i_j_i. ir. apply ex_intro with a. ap not_i_not_j. am. am. Qed.
imports: tactics