proposition: Lemma If_cond_false : forall (T : Set) (a : bool) (x y : T), x <> y -> If T a x y = y -> a = false.
proof: Proof. unfold not in |- *. simple induction a. simpl in |- *. intros. absurd (x = y). auto. exact H0. auto. Qed.
imports: Bool