proposition: Lemma forall_distr_and {A B C} : (forall x : A, B x /\ C x) <-> ((forall x, B x) /\ (forall x, C x)).
proof: Proof. split; intro H; split; intros; apply H. Qed.
imports: Coq.Program.Basics Fiat.Common.Coq__8_4__8_5__Compat