Consider these two results that say something about distributivity of implication.
∀ (f g h: Prop), (f ∨ g → h) ↔ (f → h) ∧ (g → h).
∀ T (f g h: T → Prop), (∀ x: T, f x ∨ g x → h x) ↔ (∀ x: T, f x → h x) ∧ (∀ x: T, g x → h x).
Note that they apply in different situations. For example, split_or__0ary cannot be used on a hypothesis such as H : ∀ x0 : X, x = x0 ∨ x0 ∈ l1 → x0 ∈ l2. So it seems useful to have both.
Both can be proven with the same proof script:
- intros. split.
- intros. apply H. left. assumption.
- intros. apply H. right. assumption.
- intros. destruct H. destruct H0.
- apply H. assumption.
- apply H1. assumption.
I imagine that the same proof will apply to binary predicates and further.
Can I represent this result compactly, without repetition? What should it tell me about Coq and logic in general?