blob: c6f48a0ab4bd2189608e30ff880af1f4c3feedb5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Require Import Crypto.Spec.Encoding.
Section EncodingTheorems.
Context {A B : Type} {E : canonical encoding of A as B}.
Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
Proof.
intros.
assert (dec (enc x) = dec (enc y)) as dec_enc_eq by (f_equal; auto).
do 2 rewrite encoding_valid in dec_enc_eq.
inversion dec_enc_eq; auto.
Qed.
End EncodingTheorems.
|
