proposition: Lemma COND_True (A : Type') (x y : A) : COND True x y = x.
proof: Proof. unfold COND. match goal with [|- ε ?x = _] => set (Q := x) end. assert (i : exists q, Q q). exists x. split; intro h. reflexivity. apply False_rec. rewrite <- h. exact I. generalize (ε_spec i). intros [h1 h2]. apply h1. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat