proposition: Lemma elsewhere2 : forall (x : E) (y : F), x <> x0 \/ y <> y0 -> change_x0y0 x y = t x y.
proof: Proof. intros; elim H; intros. rewrite elsewhere2_x; auto. apply f_equal with (f := fun g : E -> G => g x) (x := fun x' : E => change_x0y0 x' y) (y := fun x' : E => t x' y). apply elsewhere2_y; auto. Qed.
imports: List finite