Consider these two results that say something about distributivity of implication.

Lemma split_or__0ary:

∀ (f g h: Prop), (f ∨ g → h) ↔ (f → h) ∧ (g → h).Lemma split_or__1ary:

∀ 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:

Proof.

intros. split.

- intros. split.

- intros. apply H. left. assumption.
- intros. apply H. right. assumption.
- intros. destruct H. destruct H0.

- apply H. assumption.
- apply H1. assumption.
Qed.

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?