proposition: Lemma is_true_of_true : True = is_true true.
proof: Proof. unfold is_true. apply prop_ext. trivial. trivial. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List