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).