proposition: Lemma CorrectEncoder_Enqueue : CorrectEncoder Enqueue_Format Enqueue_Encode.
proof: Proof. unfold CorrectEncoder, Enqueue_Encode, Enqueue_Format in *; split; intros. - injections; computes_to_econstructor. - discriminate. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs