Commit fe530b1c authored by Nikita Zyuzin's avatar Nikita Zyuzin

Rename the cmd soundness statement

parent 14a2b518
......@@ -4143,7 +4143,7 @@ Proof.
- apply validErrorboundAA_sound_downcast; auto.
Qed.
Lemma validErrorboundAAcmd_sound_existential c:
Lemma validErrorboundAACmd_sound c:
forall E1 E2 A Gamma DeltaMap fVars dVars outVars
(expr_map1 expr_map2 : FloverMap.t (affine_form Q))
(noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
......
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