pub fn or_split_dc<A: Prop, B: Prop, C: DProp>( f: Imply<A, Or<B, C>>) -> Or<Imply<A, B>, Imply<A, C>>
(a => (b ∨ c)) => (a => b) ∨ (a => c).
(a => (b ∨ c)) => (a => b) ∨ (a => c)