proposition: Theorem not_January_eq_February' : January <> February.
proof: Proof. unfold not; intros H. change ((fun m:month => match m with | January => True | _ => False end) February). rewrite <- H. trivial. Qed.
imports: ZArith List Arith Bool