pub fn tauto_excm_to_or_pow<A: Prop, B: Prop>( x: Tauto<ExcM<A>> ) -> Or<Pow<A, B>, Pow<Not<A>, B>>
(a ⋁ ¬a)^true => (a^b ⋁ (¬a)^b).
(a ⋁ ¬a)^true => (a^b ⋁ (¬a)^b)