proposition: Lemma forall_impl {A B C} : (forall x : A, (impl (B x) (C x))) -> (impl (forall x, B x) (forall x, C x)).
proof: Proof. intro H; intros H' x; apply H, H'. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat