Skip to content
Snippets Groups Projects
Commit 46ffdc4a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Name some variables.

parent 2352d3a9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/bi/embedding.v
+ 1
− 1
View file @ 46ffdc4a
......@@ -45,7 +45,7 @@ Section bi_embedding.
Proof. solve_proper. Qed.
Global Instance bi_embed_inj : Inj (≡) (≡) bi_embed.
Proof.
intros ?? EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
intros P Q EQ. apply bi.equiv_spec, conj; apply (inj bi_embed);
rewrite EQ //.
Qed.
......
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