Crypto.Fancy.Montgomery256.prod_montred256_correct.Assumptions.expected
Axioms:
FunctionalExtensionality.functional_extensionality_dep : forall (A : Type)
(B : A -> Type)
(f
g : forall x : A,
B x),
(forall x : A,
f x = g x) ->
f = g