Commit 6bb6f29d authored by Robbert Krebbers's avatar Robbert Krebbers

Variant of pair_split for Leibniz equality.

parent 7c1de72a
......@@ -984,6 +984,10 @@ Section prod_unit.
Lemma pair_split (x : A) (y : B) : (x, y) (x, ) (, y).
Proof. by rewrite pair_op left_id right_id. Qed.
Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
(x, y) = (x, ) (, y).
Proof. unfold_leibniz. apply pair_split. Qed.
End prod_unit.
Arguments prodUR : clear implicits.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment