proposition: Lemma Prop_bool_eq (P : Prop) : P = @COND bool P true false.
proof: Proof. assert (P = True \/ P = False). apply prop_degen. destruct H. rewrite H. rewrite (COND_True bool true false). rewrite is_true_of_true. reflexivity. rewrite H. rewrite (COND_False bool true false). rewrite is_true_of_false. reflexivity. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List Coq.Strings.Ascii