proposition: Lemma CorrectEncoder_StrictTerminal : CorrectEncoder StrictTerminal_Format StrictTerminal_Encode.
proof: Proof. unfold CorrectEncoder, StrictTerminal_Format, StrictTerminal_Encode; split; intros. - injections; repeat computes_to_econstructor; eauto using measure_mempty. - discriminate. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Vectors.Vector Fiat.Computation Fiat.Narcissus.Common.Specs