proposition: Lemma refine_format_SumType {m} (types : Vector.t Type m) (formats : ilist (B := fun T => T -> CacheFormat -> Comp (B * CacheFormat)) types) (encoders : ilist (B := fun T => T -> CacheFormat -> (B * CacheFormat)) types) (st : SumType types) (ce : CacheFormat) : Iterate_Ensemble_BoundedIndex' (fun idx => forall a ce, refine (ith formats idx a ce) (ret (ith encoders idx a ce))) -> refine (format_SumType types formats st ce) (ret (encode_SumType types encoders st ce)).
proof: Proof. intros. unfold format_SumType, encode_SumType; simpl. remember (SumType_proj types st); clear Heqn. revert n ce; pattern (SumType_index types st). eapply Iterate_Ensemble_equiv'. apply H. Qed.
imports: Fiat.Common.ilist Fiat.Common.SumType Fiat.Common.IterateBoundedIndex Fiat.Narcissus.Common.Specs Coq.Sets.Ensembles Bedrock.Word