proposition: Lemma ex_distr_or A B C : (exists x : A, B x \/ C x) <-> ((exists x : A, B x) \/ (exists x : A, C x)).
proof: Proof. repeat ((intros [H0 H1]; revert H0 H1) || (intros [H|H]; revert H) || split || intro); first [ do 2 first [ left | esplit ]; eassumption | do 2 first [ right | esplit ]; eassumption ]. Defined.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat