diff options
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index aea3ff4c2..511370c63 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -387,9 +387,7 @@ Definition decode (x : fe25519) : F modulus Lemma proj1_fe25519_encode x : proj1_fe25519 (encode x) = ModularBaseSystem.encode x. -Proof. - hnf in x; destruct_head' prod; reflexivity. -Qed. +Proof. reflexivity. Qed. Lemma decode_exist_fe25519 x pf : decode (exist_fe25519 x pf) = ModularBaseSystem.decode x. |