proposition: Lemma involutive : forall i j a : E, create i j (create i j a) = a.
proof: Proof. ir. apply by_cases with (a = i). ir. rewrite H. rewrite i_j_i. ap i_j_j. apply by_cases with (a = j). ir. rewrite H. rewrite i_j_j. ap i_j_i. ir. pose (not_i_not_j H0 H). rewrite e. am. Qed.
imports: tactics