Function prop::eq::true_eq

pub fn true_eq<A: Prop>(a: A) -> Eq<A, True>

There is an a : A is the same as A being true.

With other words, a proof means it is true, and if it is true then there is a proof.