proposition: Lemma case_ineq : forall (E F : Set) (eq_E_dec : eq_dec E) (x x' : E) (y z : F), x <> x' -> match eq_E_dec x x' with | left _ => y | right _ => z end = z.
proof: Proof. intros; case (eq_E_dec x x'). intros; absurd (x = x'); auto. trivial. Qed.
imports: Arith Omega List