blob: f194b442b73bbe3ff1e5d1cf3a700836169cc9e1 (
plain)
1
2
3
4
5
|
Require Export Crypto.Util.FixCoqMistakes.
Lemma pull_prod_forall A A' B B' (Q : A * A' -> B * B' -> Prop)
: (forall x y, Q x y) <-> (forall x0 y0 x1 y1, Q (x0, x1) (y0, y1)).
Proof. intuition. Qed.
|