pub fn tauto_excm_to_or_pow<A: Prop, B: Prop>(
    x: Tauto<ExcM<A>>
) -> Or<Pow<A, B>, Pow<Not<A>, B>>
Expand description

(a ⋁ ¬a)^true => (a^b ⋁ (¬a)^b).