proposition: Lemma pred_conj_forall_distrib : forall A (P Q: A->Prop), ((forall x, P x) /\ (forall x, Q x)) = (forall x, P x /\ Q x).
proof: Proof. Proof using. intros. apply prop_ext. iff H. autos*. split; intros x; apply* (H x). Qed.
imports: TLC(LibTactics)