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