proposition: Lemma enc_readingCorrect : CorrectAlignedEncoder format_reading enc_reading.
proof: Proof. unfold enc_reading, format_reading. eapply refine_CorrectAlignedEncoder. 2: eapply CorrectAlignedEncoderForFormatMChar_f; eauto. intros; destruct s; simpl; rewrite refine_Projection_Format; split; try reflexivity; intros; eapply format_word_inhabited'; intros; eauto. Qed.
imports: Fiat.Narcissus.Examples.TutorialPrelude