proposition: Lemma ex_ind_iff {T P} {Q : _ -> Prop} : (forall pf : @ex T P, Q pf) <-> forall (x : T) (y : P x), Q (ex_intro P x y).
proof: Proof. intuition; destruct_all (ex P); auto. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat