Helper

test_recv_dec_eq

Section recv_dec_enc_tests

Type Lemma

Proof Lines 1

Lemma test_recv_dec_eq : test_recv_dec = PRecv 0 (fun x => match decrypt dk x with Some v => PRet v | None => PFail end).

* Verify the desugaring is correct

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...