Commit 19b5051a authored by Dmitry Khalanskiy's avatar Dmitry Khalanskiy

Rename parameters in due to conventions

parent 902f5305
......@@ -1204,7 +1204,7 @@ Section prod_unit.
Canonical Structure prodUR := UcmraT (prod A B) prod_ucmra_mixin.
Lemma pair_split (x : A) (y : B) : (x, y) (x, ε) (ε, y).
Lemma pair_split (a : A) (b : B) : (a, b) (a, ε) (ε, b).
Proof. by rewrite -pair_op left_id right_id. Qed.
Lemma pair_split_L `{!LeibnizEquiv A, !LeibnizEquiv B} (x : A) (y : B) :
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