proposition: Lemma even_odd_excl: forall x:X, ~(X_even x /\ X_odd x).
proof: Proof. intro. assert (X_even x -> ~ X_odd x). 2:tauto. pose proof (X_even_coind (fun x:X => ~ X_odd x) (fun y:Y => ~ Y_even y)). apply H. intuition. destruct H1. apply H0 with y. reflexivity. intuition. inversion H2. apply g_inj in H3. apply H1. rewrite <- H3. assumption. intuition. inversion H2. apply H3 with x0. reflexivity. apply f_inj in H3. apply H1. rewrite <- H3. assumption. Qed.
imports: FunctionProperties DecidableDec Description Classical