Function prop::imply::or_split_excm_a
source · pub fn or_split_excm_a<A: Prop, B: Prop, C: Prop>(
f: Imply<A, Or<B, C>>,
excm_a: ExcM<A>
) -> Or<Imply<A, B>, Imply<A, C>>
Expand description
(a => (b ∨ c)) ⋀ (a ⋁ ¬a) => (a => b) ∨ (a => c)
.