proposition: Lemma is_True P : (P = True) = P.
proof: Proof. apply prop_ext. intro e. rewrite e. exact I. apply PropExt_imp_ProvPropExt. intros a b [ab ba]. apply prop_ext. apply ab. apply ba. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts