proposition: Lemma is_true_of_false : False = is_true false.
proof: Proof. unfold is_true. apply prop_ext. auto. intro. discriminate. Qed.
imports: Coq.Logic.ClassicalEpsilon ClassicalFacts PropExtensionalityFacts Lia PeanoNat ProofIrrelevance ExtensionalityFacts List