proposition: Lemma COND_def {A : Type'} : (@COND A) = (fun t : Prop => fun t1 : A => fun t2 : A => @ε A (fun x : A => ((t = True) -> x = t1) /\ ((t = False) -> x = t2))).
proof: Proof. exact (eq_refl (@COND A)). Qed.
imports: coq theory_hol types